Technical topic: SDL2IF/OBS2IF
Contents
Introduction
sdl2if translates SDL processes representing the behavior of TASTE functions or TASTE observers into respectively IF processes or IF observers.
sdl2if is developed as a back-end of OpenGEODE, from which it re-uses the SDL parser and the AST representation. It is developed in Python 3.x and uses single-dispatch generic functions (functools/singledispatch) to structure the translation.
Usage
sdl2if is invoked as follows
$ sdl2if [--output-dir dir] file1.pr [ ... file_n.pr]
and produces a unique .if file containing the translation of the SDL process defined in file1.pr (... file_n.pr) as an IF process. The file will be created in the output-directory if specified, else in the current working directory. The name of the .if file is the lowercase name of the SDL process.
Key Features
- supports a significant part of SDL including expressions on data variables with ASN.1 types, hierarchical and parallel states, inner procedures, task for loops, decisions, floating labels, etc
- preserves the structure of the input model, that is, each SDL concept is mapped 1-to-1 into an equivalent IF concept, whenever possible - e.g., variables, hierarchical states, transitions, actions - and therefore facilitates the inspection and the understanding of the generated code
- preserves the operational semantics, that is, traceability between executions in TASTE and executions in IF, as much as possible
- generates IF processes slightly optimized for exhaustive model-checking, by limiting the increase of the state vector and/or state space due to auxiliary variables
- in observers, supports success, error and ignore states
- in observers, supports both simple and generic input/output transition triggers; the generic triggers are expanded at translation using auto-generated -Event types in observer.asn
- in observers, translates SDL timers as IF clocks and allow checking properties dealing explicitly with real time
Known Limitations
- no entry/exit procedures in hierarchical state machines
- no mutually recursive inner procedures
- no 'NEXTSTATE -' in transitions from / with floating labels
- restricted input/output event triggers and/or system state expressions in observers
Examples
An SDL process
process memoryscrub(1); var running boolean := true public; var sender pid := nil; var par EnableDisable public; state start #start ; task running := false; nextstate disabled; endstate; state disabled; input memoryscrub_enableordisable (par, sender); nextstate u_decision_1; endstate; state u_decision_1 #unstable ; provided (par = EnableDisable_scrubon); task running := false; nextstate enabled; provided (par = EnableDisable_scruboff); task running := false; nextstate disabled; endstate; state enabled; input memoryscrub_enableordisable (par, sender); nextstate u_decision_2; provided (not running) and true; task running := true; informal "input_none"; // writeln ; task running := false; nextstate enabled; endstate; state u_decision_2 #unstable ; provided (par = EnableDisable_scrubon); task running := false; nextstate enabled; provided (par = EnableDisable_scruboff); task running := false; nextstate disabled; endstate; endprocess;
An SDL observer
intrusive observer droppick; var running boolean := true public; var sender pid := nil; var aux_signal t_if_signal; var cmd Roboticarmstatus public; state start #start ; task running := false; nextstate wait; endstate; state checkdrop; provided (not running); match input rarmcontrol_roboticarm_request (cmd, sender) in {rarmcontrol}0; task running := true; nextstate u_decision_1; endstate; state u_decision_1 #unstable ; provided (cmd.predicate = RoboticarmPred_roboticarm_picking); task running := false; nextstate error; provided (cmd.predicate = RoboticarmPred_roboticarm_dropping); task running := false; nextstate wait; provided not ((cmd.predicate = RoboticarmPred_roboticarm_picking) or (cmd.predicate = RoboticarmPred_roboticarm_dropping)); task running := false; nextstate checkdrop; endstate; state error #error ; endstate; state wait; provided (not running); match input rarmcontrol_roboticarm_request (cmd, sender) in {rarmcontrol}0; task running := true; nextstate u_decision_2; endstate; state u_decision_2 #unstable ; provided (cmd.predicate = RoboticarmPred_roboticarm_picking); task running := false; nextstate checkdrop; provided (cmd.predicate = RoboticarmPred_roboticarm_dropping); task running := false; nextstate error; provided not ((cmd.predicate = RoboticarmPred_roboticarm_picking) or (cmd.predicate = RoboticarmPred_roboticarm_dropping)); task running := false; nextstate wait; endstate; endobserver;
Transformation Rules
Declarations
State Machines
States
Labels
Inner Procedures
Actions
Input
Continuous Signal
Task
Output
Procedure Call: Inner SDL Procedure
Procedure Call: External Protected Interfaces (C Implementation)
Writeln
Set, Reset
Decision
Terminator
Comment
Expressions
Constants
Binary Operators
Conditional Expressions
Math Operators
Sequence/Of Operators
Choice Operators
Other Operators
Implementation
The sdl2if implementation is located under the Taste / IF Model Checking git repository within the modules/sdl2if directory.
The tool entry point is defined within sdl2if.py and the core implementation is located within IfGenerator.py. At top level, sdl2if uses the opengeode parser to construct the AST of the input SDL files, then it proceeds with the transformation on the first SDL process, by doing:
ast, warnings, errors = opengeode.parse(options.files) IfGenerator.generate(ast.processes[0], output_dir=options.output_dir)
The implementation of the model transformation is recursive on the AST representation of the SDL process as constructed by opengeode. Single-dispatch generic functions are used to handle the various AST objects, and produce (fragments of) the IF process(es) and related IF definitions, as summarized below:
Function | ogAST Classes |
---|---|
tr_process | ogAST.Process, ogAST.Procedure |
tr_state_machine | ogAST.Process, ogAST.CompositeState, ogAST.Procedure |
tr_state | ogAST.Process, ogAST.CompositeState, ogAST.Procedure, ogAST.FloatingLabel |
tr_transition | ogAST.Input, ogAST.ContinuousSignal, ogAST.Transition, ogAST.Terminator |
tr_action | ogAST.Input, ogAST.ContinuousSignal, ogAST.Label, ogAST.Task*, ogAST.Output, ogAST.ProcedureCall, ogAST.Decision |
tr_expression | ogAST.Expr*, ogAST.Prim* |
The resulting IF process(es) and related definitions are represented using dedicated data structures. That is, in a first step, an IF model is progressively constructed while traversing the AST, then, in a second step, the IF model is written into a textual .if file.
The implementation provides the classes IfSignal, IfVariable, IfGuard, IfAction, IfTransition, IfState, IfProcess to represents structurally the corresponding IF concepts. In addition, the class IfWeb allows to store an IF state machine fragment with potentially any number of pending entry and exit transitions and provides specific methods to glue such fragments into bigger ones, ultimately leading to complete state machines.
Finally, the implementation relies on several helper functions with dedicated functionalities, the most important being summarized in the table below:
Functions | Provided Functionality |
---|---|
ctxt_* | access information about the transformation context |
if_*_name | get names for different concepts at IF level |
idx_* | unique indexing of AST objects |
auxvar_* | handling auxiliary variables |
forloopvar_* | handling ogAST.TaskForLoop variables |
inosig_* | output forwarding from inner procedures |
is_input_*, *_discard_* | auto-completion with discard transitions |
*_observer_*, *_match_* | observer specific access and/or transformation |
Extensions
In general, extending the transformation for a new AST concept would require the implementation of the corresponding transformation function(s), in the appropriate category(-ies). Nevertheless, extending the transformation with a new predefined call expression operator can be simpler:
- if the new operator is going to be supported in IF through a (homonym) abstract function (with extern C implementation) then, it would be enough to extend the list of predefined operator names defined within tr_expression // _prim_call so that to include the new operator name,
- otherwise, if the new operator is going to be supported by built-in expansion into an IF expression then, this operator shall be handled specifically within the tr_expression // _prim_call, in a similar way as the operators present, exists, etc.