ReaX: User Manual
Contents
1. lt assertion gt assertion lt expr gt lt initial gt initial lt expr gt lt final gt final lt expr gt lt invariant gt invariant lt expr gt lt reach gt reachable lt expr gt lt attract gt attractive lt expr gt Note that zeroadic nodes i e without any input nor controllable sections are admitted Further non controllable nodes Ctrld i e without any controllable section are also valid Transition Function Definitions The transition function of nodes are specified as assign ments of state variables according to the following syntax trans funec gt i transition lt assign gt lt assign gt assigns iiS lt id gt r TI expres 17 2 4 2 Weavable Function Specification Ctrlf A Controllable Nbac function defines output vectors based on inputs Its grammar is as defined by the lt func gt rule bellow Main rule lt func gt lt typdefs gt lt func decls gt lt local defs gt lt func formulas gt Variable declaration sections lt func decls gt lt io groups decl gt lt local decls gt Optional assertion on inputs amp outputs lt func formulas gt lt assertion gt Zeroadic functions i e without any input nor output sections are not admitted 2 4 3 Weavable Predicate Specification Ctrlp CtrIr A Controllable Nbac predicate is a Boolean function without state Its gramma2. 0 087 d sB K 43n 177m lt G gt NANG 0 087 I Synth logico numerical synthesis with powerset extension of power domain over intervals with BDDs succeeded 0 089 I Env CUDD reordering 0 102 I t Triangulation 0 102 D ts U C group 1 cl not _cl and not sl and tl Active and x1 9 gt 0 or _cl c2 not _c2 and not rl and not s2 and t2 Active and x2 9 gt 0 or not _c2 and not cl and rl and not s2 and t2 Active and x2 9 gt 0 or not _c2 and cl and rl and not s2 and t2 Active or _c2 and not rl and t1 Idle or _c2 and not cl and rl and tl Idle or _c2 and cl and rl and not r2 and tl Idle or _c2 and cl and rl and r2 and tl Idle and t2 Active or _c2 and not cl and not r2 and not sl and tl Active or _c2 and cl and not sl and tl Active or _c2 and sl and tl Active 0 104 I Main Extracting triangularized controller 0 105 I Main Checking triangularized controller 0 107 I Main Outputting into 2tasks counters ctrlf From this trace one can observe the successive values computed and notably the set of states to be effectively avoided I Note that the BDD representation of the controller K is printed in abbreviated form as it is quite large still a representation of the triangularized controller assignments of cl and c2 is shown at the end of the trace In Controllable Nbac format the resulting triangularized controller file 2tasks counters ctrlf is 2tasks
3. reals 41 4 lt digit gt lt digits gt s 18 Et J D 1 p digits Identifiers lt id gt lt id character gt lt id character gt lt digit gt 4id character gt irs A At tat er J tr J te 2 3 2 Expressions Numerical constants are specified as usual and the Boolean ones are true and faise Although grammar rules do not impose any typing constraints on expressions some type checking is performed during parsing and typing errors reported by ReaX may be interleaved with syntax related ones Boolean constants best gt i244 true false Numerical constants lt ncest gt iis lt positive gt lt rational gt lt real gt lt bint gt bint gt lt bint type gt lt positive gt Untyped expressions lt expr gt lt boest gt lt nest gt lt id gt lt unary operator gt lt expr gt lt expr gt lt binary operator gt lt expr gt if lt expr gt then lt expr gt else lt expr gt lt exprs list gt eneste ids lt 6 xpr gt in eexpres list gt lt exprs y lt exprs list gt lt expr gt lt expr gt Available operators lt unary operator gt not lt binary operator gt z tang l re F a l Regg l eq l ae t l UE a l Fa Vel ist Wenn gt l lt gt l tai and in operators are syntactic sugar to encode respectively the mu
4. x2 gt 11 0 055 d sS pre tl Idle and t2 Active gt x2 gt 10 tl Idle and t2 Active gt x1311 A x2 lt 9 13 0 0 0 0 0 O 0 0 0 0 057 057 066 069 069 078 081 082 083 083 085 086 087 ss ss ss ss ss ss nn s ss sB sB tl Active and t2 Idle gt x2 gt 11 tl Active and t2 Idle x1310 A x2 lt 10 tl Idle and t2 Idle x2 gt 11 tl Active and t2 Active x1310 A x2 lt 9 tl Idle and t2 Idle gt x1311 A x2 lt 10 tl Active and t2 Active x2 gt 10 Traversing arc 1 B tl Active and t2 Active gt x2 gt 10 x2 gt 11 tl Active and t2 Idle gt x1310 A x2 lt 10 tl Active and t2 Active x1 lt 10 A x2 lt 10 tl Idle and t2 Active gt x2 gt 10 tl Active and t2 Active x1310 A x2 lt 9 x1211 A x2 lt 10 pre tl Idle and t2 Active gt x2 gt 10 tl Idle and t2 Active gt x1311 A x2 lt 9 tl Active and t2 Idle gt x2 gt 11 tl Active and t2 Idle gt x1310 A x2 lt 10 tl Idle and t2 Idle gt x2211 tl Active and t2 Active x1310 A x2 lt 9 tl Idle and t2 Idle x1311 A x2 lt 10 tl Active and t2 Active x2 gt 10 Traversing arc 1 B tl Active and t2 Active gt x2 gt 10 x2 gt 11 tl Active and t2 Idle x1310 A x2 lt 10 tl Active and t
5. In case the vector of state variables involves numerical variables one should consider using the approximating algorithm with abstract interpretation To do so one should use the sS algorithm specifier Available flags for this algorithm are listed in Table 3 and options are listed in Table Table 3 Flags specific to the approximating synthesis algorithm split Perform the split algorithm for handling of non convex set of forbidden states may lead to deadlocks in the result bdisj Force full DNF decomposition of forbidden states predicate when using the split algorithm Table 4 Options specific to the approximating synthesis algorithm d Abstract domain specification cf Section 3 3 below ws Maximum number of ascending iterations before resorting to base widening wd Number of descending iterations after base widening 3 3 Available Abstract Domains Abstract domains are specified in a way similar to synthesis algorithms and all share a common set of options The first component of abstract domains is the numerical abstraction that can be specified using one selector of Table 5 After having chosen the numerical domain several flags and options are available that are listed in Table 6 Table 7 lists additional options for the convex polyhedra numerical abstract domain Table 5 Numerical abstract domain selectors I Intervals Boxes Octagons P Convex Polyhedra Table 6 Options for abstract domain
6. Berthier and Marchand 2014 In terms of behavior the main difference lies in the ability of the controller to force entering Idle from Active Its automaton representation is shown in Figure 1 rAc A r Ac 1st tn 4 s Vc sVC Figure 1 Task automaton 2tasks ctrin typedef S enum Idle Active state tly E26 53 input rl r2 sl s2 cl bool controllable ol 7 cly c2 7 clt Bool Itransition tl if tl Idle and rl and cl then Active else 10 if tl Active and sl or cl then Idle else t1 t2 if t2 Idle and r2 and c2 then Active else if t2 Active and s2 or c2 then Idle else t2 initial tl Idle and t2 Idle invariant t1 Active t2 Active Remark that in this example the default value for controllable input c1 is specified as additional non controllable input _c1 for illustrative purpose the default value of c2 is the effective value of c1 to be chosen by the controller Executing ReaX for Boolean Synthesis To compute a controller for this node using the Boolean synthesis algorithm sB to triangularize it t and also to show basic debugging information about the execution of ReaX debug D one can use the following command line reax 2tasks ctrin a sB t debug D The program reports on its execution using a sequence of log entries as listed bellow Each log entry starts with a measure of the time it effectively used the processor since the beginning of it
7. a2 Common Flags ouaaa a 7 3 2 2 Boolean Synthesis SB aaa eee eee ee ee 8 3 2 3 Approximating Synthesis s S eek a aaa 8 3 3 Available Abstract Domains o aaa a 8 ee ee ee 9 3 4 1 One step Optimization 00 0000 9 3 4 2 Triangularization 2 0 02 eee ee eee 9 3 4 3 Triangularization amp Merging 000 10 3 5 Example Executions asc 4A R42 RAGE RENEE be RES 10 3 9 1 Finite state Case o s sic e eee ek eee Re i Se a 10 3 5 2 _Infinite stateCase 2 2 ee 12 3 5 3 Synthesizing Towards Simulation 16 17 18 1 Installation Instructions 1 1 External Library Dependencies ReaTK and most of its dependencies are written using OCaml yet some of its library depen dencies require a decent version of GCC to be compiled as well as development packages of GMP and MPFR libraries packages 1ibgmp dev and libmprf dev under Debian based distributions gnp devel and mpfr devel under Fedora 1 2 Installation using OPAM The recommended way for installing ReaTK is to use the OCaml Package Manager OPAM See http people irisa fr Nicolas Berthier opam for further instructions 1 3 Manual Compilation Please refer to the README file at the root of the source tree 2 The Controllable Nbac Language 2 1 Naming Conventions The tool ReaX handles input files that must define either a node a function or a predicate By conventio
8. counters ctrlif typedef S enum Idle Active input CL S7 E24 83 xl int x2 ints rl bool r2 bool sl bool s2 bool cls booli 2 pool Soutput cl bool eZ bool local 10 bool 11 bool 12 bool 13 bool 14 bool 15 bool 16 bool 17 Booly 15 18 bool 19 bool 110 pool 111 bool 1127 Bool 113 Bool 114 bool 115 Bool 116 bool 117 bool definition 10 not sl 13 not s2 14 t2 Active 19 not r2 112 not rl 11 10 and x1 gt 9 15 13 and 14 114 19 or 14 12 t1 Active and 11 x2 gt 9 and 15 cl or 12 17 if cl then 15 else 16 cl or 19 not cl 18 if rl then 17 else 16 1 s1 or 110 115 113 or 114 6 7 Q H font II 112 or 115 17 if t1 Idle then 116 else 111 c2 if _c2 then 117 else 18 assertion true 3 5 3 Synthesizing Towards Simulation Using the same example node as in the previous Section one can also leave the controller in its predicate form Ctrlr and use the tool ctrl2lut also available as OPAM packagd to generate a stochastic reactive program from the controlled node as a whole reax 2tasks counters ctrin a sS d 1I D deads produces the controller as a predicate in file 2tasks counters ctrIr Interactive Simulation From this step the command ctrl2lut o two tasks counters lut 2tasks counters ctrln 2tasks counters ctri
9. 0 and x2 0 invariant t1 Active t2 Active and x1 lt 10 and x2 lt 10 It encodes the parallel composition of two instances of the automaton of Figure 2 Here the invariant to enforce is both the mutual exclusion between the Active states and the bounding of their counters Figure 2 Task automaton with counter Executing ReaX for Over approximating Synthesis To compute a controller for this node using the deadlock avoiding over approximating synthesis algorithm sS deads with the disjunctive power domain over intervals d I D and then triangularize it t we use the following command line reax 2tasks counters ctrin a sS d 1I D deads t debug D2 The corresponding rather detailed execution trace debug D2 shows 0 023 I Main Reading node from 2tasks counters ctrin 0 046 I Supra Variables bool num state 2 2 i 8 0 u 6 0 c 2 0 0 046 I Df2cf Preprocessing discrete program 0 046 I Verif Forcing selection of power domain 0 047 I Synth logico numerical synthesis with powerset extension of power domain over intervals with BDDs 0 047 D Computing the original set of deadlocking states 0 048 d sS a t1 Active and t2 Active gt x1 lt 10 A x2 lt 10 x2 gt 11 x13 gt 11 A x2 lt 10 0 049 d s Beginning of least fixpoint computation 0 049 d sS Traversing arc 1 0 049 d sS B x1211 A x2 lt 10 tl Active and t2 Active x1 lt 10 A x2 lt 10
10. 2 Active x1 lt 10 A x2 lt 10 tl Idle and t2 Active gt x2 gt 10 tl Active and t2 Active x1310 A x2 lt 9 x1211 A x2 lt 10 pre tl Idle and t2 Active x1311 A x2 lt 9 tl Idle and t2 Idle gt x2211 tl Active and t2 Active x1310 A x2 lt 9 tl Active and t2 Idle gt x1310 A x2 lt 10 tl Idle and t2 Idle x1311 A x2 lt 10 tl Active and t2 Active x2 gt 10 tl Idle and t2 Active gt x2 gt 10 tl Active and t2 Idle gt x2 gt 11 End of least fixpoint computation a 1 x2 gt 11 x1211 A x2 lt 10 t1 Idle and t2 Active gt x2 gt 10 t1 Active and t2 Active gt x1310 A x2 lt 9 tl Active and t2 Idle x1310 A x2 lt 10 t1 Active and t2 Active gt x2 gt 10 t1 Active and t2 Active gt x1 lt 10 A x2 lt 10 ATi Ere I 8 Jtl Active and t2 Active x1 lt 10 A x2 lt 10 tl Active and t2 Idle x1310 A x2 lt 10 t1 Idle and t2 Active gt x2310 x2 gt 11 x1211 A x2 lt 10 tl Active and t2 Active gt x1310 A x2 lt 9 tl Active and t2 Active gt x2 gt 10 y t1 Idle and t2 Idle and x2 10 gt 0 and x1 10 gt 0 or tl Idle and t2 Active and x2 10 gt 0 and x1 10 gt 0 and x2 9 gt 0 or tl Active and t2 Idle and x2 10 gt 0 and x1 10 gt 0 and x1 9 gt 0 G Building controller Computing boundary transtions 14 0 087 I sB Simplifying controller
11. ReaX User Manual Nicolas Berthier April 30 2015 ReaTK is the Reactive System Verification and Synthesis ToolKit It provides the ReaVer tool dedicated to the static verification of logico numerical programs by abstract interpretation and the ReaX tool performing discrete controller synthesis for such programs This manual details the ReaX tool by means of a small example and some expla nations about its usage Contents 1_Installation Instructions 1 1 External Library Depetidencics lt 5n 6 nee b 4 Hoe oO Se ee ee EO 1 2 Installation using OPAM 0 00 eee ee eee 1 3 Manual Compilation 0 200 200 0002 0000 2 The Controllable Nbac Language 2 1 Naming Conventions 0 0 a 2 2 Global Structure ooa ee 23 Common Rules ss sys er s aoea aa e ee 2 3 1 LexingRules ooa 2 20 0 0 0 eee 2 3 2 Expressions 1 ee ee ee ee 2 3 4 Variable Declarations 00000 e eee eee 2 3 5 Local Variable Declaration and Definitions 2 3 6 Declaring Weavable Signatures 000 2 4 Main Entities 2 E a EA a a A E E R 2 4 1 Weavable Node Specification Ctrln Ctrld 2 4 2 Weavable Function Specification Ctrlf 0 2 4 3 Weavable Predicate Specification Ctrlp Ctrlr 2 2 2 5 Variable Scope TODO x NyNNN NDDADAA NHB BPwWwwWBwWWDHD N 7 SHAH RASS Oa ER EEE SS Bee WSS 7 ok ek eo BER A eee 7
12. act also referred to as Boolean and an approximating one The former is dedicated to operate on finite state systems and the latter is capable of handling infinite ones 3 2 1 Common Flags Table i lists the flags that are common to all synthesis algorithms Table 1 Flags that are common to all synthesis algorithms deads Exclude initial deadlocking states from the invariant nobnd Disable computation of boundary transitions in the controller 3 2 2 Boolean Synthesis sB If the input node does not comprise any numerical state variable then the exact synthesis algorithm can be used to compute a controller The descriptor for this algorithm is sB and its additional flags are given in Table 2 Note that reachable and attractive sections of the input Table 2 Flags specific to the Boolean synthesis algorithm r Enable reachability property enforcement a Enable attractivity property enforcement may be buggy for now node are ignored by ReaX unless the corresponding flag is explicitly set Audacious Usage Notice that the Boolean synthesis algorithm may compute correct results for nodes involving numerical components in their vector of state variables even if these state variables do not encode outputs see Section A Note on Specifying Outputs of the Technical References Manual It may however never terminate and lead to an explosion of memory consumption in this case 3 2 3 Approximating Synthesis sS
13. cal variable transitively inherits the minimal scope among the variable dependencies of its expression definition See Section 2 5 for details about variable scopes 2 3 6 Declaring Weavable Signatures Non controllable Variable Declarations A set of non controllable variables must be de clared within an input section Declaration of non controllable variables lt input decls gt input lt var decls gt Controllable Variable Declarations The declaration of a sequence of controllable variables takes place in controllable sections and additionally permits the specification of associated default expressions Declaration of controllable variables seri l decls gt tim controllabile lt eirl declse gt lt ctri decis gt 2etril decle t lt cirl lt ide i lt etrl id gt r type 3 ctri id gt r lt id gt expr U C groups Specification U C groups are declared by alternating input and controllable sections Possibly empty sequence of U C groups lt uc groups decl gt iis lt uc group decl gt L lt uc group final u gt lt uwe greup only e gt lt uc group decl gt ifs lt input decls gt lt ctrl decls gt lt uc group final u gt lt input decls gt suc group only c gt i lt ctri decls U C group sequences must start with the declaration of a set of non controllable inputs unless all inputs are controllable I O groups Specification I O groups are the c
14. composition b m Select BDD based MTBDD based composition default is BDD based MTBDD based is generally less efficient yet it might perform better for disjunctive domains Table 7 Convex polyhedra options s l Select Strict Loose convex polyhedra 3 4 Post processing the Controller A successful synthesis produces a controller Ctrlr in the form of a predicate over the signature of the initial node state variables plus inputs As noted in Section Synthesis Product s o the Technical References Manual this predicate is non deterministic Several possibilities exist to reduce this non determinism and even to make a function i e executable code out of it Computation steps performed on controllers computed using one of the DCS algorithms above are called post processing steps 3 4 1 One step Optimization One step optimization can be used to reduce the level of non determinism of the controller by restricting its possible choices according to given criteria For instance a controlled system whose controller has undergone one step minimization of a state variable x will always enter one of the immediate successor states for which the value of x is the smallest ReaX implements one step minimization and maximization of numerical state variables that can be triggered by using the O command line flag followed by an optimization specification of the form ol lt specs gt where lt specs gt is a sequence ex
15. n file names of node function and predicate should be suffixed with ct rln ctrlf and ctrlp respectively The file name extension ct r1d can be used for nodes without controllable input variables typically for synthesis results and ctrlr can also denote predicates 2 2 Global Structure Each of these types of inputs have a signature and a body Signatures always define name and type input variables signature of nodes additionally specify state variables The body is essentially a set of assignments for state and or output variables possibly along with definitions for local variables Controllable Nbac files are divided into sections each of which beginning with a keyword z starting with a 2 3 Common Rules Let s first define basic lexing and grammar rules that are common to any category of input understood by Reax 2 3 1 Lexing Rules The Controllable Nbac language is case sensitive and variables and type names are defined classically as identifiers Yet one shall always start label names with an uppercase letter and variable names with any other allowed identifier character Comments start with end with and can be imbricated Note all rules bellow are lexing ones no space is allowed in between characters Numbers edigit gt iis g 9 lt digits gt lt digit gt lt digit gt lt positive gt lt digits gt lt rational gt lt digits gt lt digits gt
16. nters ctrin a sS d I D deads 0O ol min xl min x2 References Berthier N and Marchand H 2014 Discrete controller synthesis for infinite state systems with ReaX In 12th Int Workshop on Discrete Event Systems WODES 14 3See http www verimag imag fr Lurette 107 html 17 Index abstract domain 8 controllable variable Controllable Nbac function 6 I O group keyword enum in node 6 predicate 6 section assertion 6 attractive 6 controllable definition final 6 initial 6 input invariant 6 local output reachable 6 state 6 transition 6 typedef value 6 U C group default expression 5 synthesis algorithm 7 approximating Boolean 18
17. ounterpart of U C groups and typically define the signature of a function resulting from the triangularization of a controller synthesized for a weavable node I O groups are declared by alternating input and output sections Non empty sequence of I O groups lt io groups decl gt lt io group decl gt lt io group final i gt lt io group only o gt lt io group decl gt lt io group decl gt lt io group decl gt lt io group decl gt lt input decls gt lt output decls gt lt io group final i gt lt input decls gt lt io group only o gt lt output decls gt lt output decls gt output lt var decls gt I O group sequences must start with the declaration of a set of non controllable inputs unless all inputs are controllable 2 4 Main Entities 2 4 1 Weavable Node Specification Ctrin Ctrld A Controllable Nbac node is specified as an input stream whose syntax is as defined by the lt node gt rule bellow Main rule lt node gt lt typdefs gt lt node decls gt lt local defs gt lt trans func gt lt node formulas gt Variable declaration sections lt node decls gt lt state decls gt lt uc groups decl gt lt local decls gt lt state decls gt state lt var decls gt Node formulas definitions lt node formulas gt lt assertion gt lt initial gt lt final gt lt invariant gt lt reach gt lt attract gt
18. pressing priority of goals that are listed in Table 8 See Section Exemplifying One step Minimization on page 17 for an example usage of this feature 3 4 2 Triangularization ReaX is able to triangularize the controller using the default expressions for controllable in puts to produce a function as detailed in Section Section Triangularization Procedure of the DoS O E Table 8 One step optimization goals available min v Minimization of numerical state variable v max v Maximization of numerical state variable v echnical References Manual Triangularization of the controller is performed when the t or t riang flag is given on the command line In this case a Controllable Nbac function is produced Ctrlf 3 4 3 Triangularization amp Merging Additional post processing can be carried out when the m or merge flag is given this flag forces triangularization In such a case the controllable inputs involved in the transition function of the original node are substituted with the corresponding equation resulting from the triangularization The output of ReaX then becomes a classical non controllable node Ctrld 3 5 Example Executions 3 5 1 Finite state Case Example Controllable Nbac Node Let the file 2t asks ctr1n exclusively contain the Controllable Nbac code as listed bellow It describes a node almost equivalent to the one described as Figure 3 in the paper introducting ReaX
19. r creates a Lutin file file two tasks counters lut that can then be simulated using the appropriate toolg For instance one can simulate the above controlled system by executing Luciole to interactively set all inputs of the system at each step main is the name of the main node in the generated Lutin program 1See http people irisa fr Nicolas Berthier opam ctrl2lut See http www verimag imag fr Lutin htm 16 lutin n main luciole two tasks counters lut Although Lutin does not support non Boolean finite variables i e enumerations for now ctrl2lut is able to handle them it one hot encodes such variables to keep the input and output signals readable Note however that finite numerical variables are not supported Automated Simulation Alternatively one can also use the ctrl2lut tool to generate a stochas tic environment node generating the inputs of the controller or original node from the values of its state variables and by ensuring that its assertion is not violated ctrl2lut o two tasks counters lut 2tasks counters ctrin 2tasks counters ctrlir e eo two tasks counters env lut In this case the simulation can be launched using Lu rettd lurettetop rp sut lutin two tasks counters lut main rp env lutin two tasks counters env lut env Exemplifying One step Minimization To perform one step optimization targeting the minimization of x1 and then of x2 one can use reax 2tasks cou
20. r is as defined by the lt prea gt rule bellow Main rule lt pred gt lt typdefs gt lt pred decls gt lt local defs gt lt pred def gt Variable declaration sections lt pred decls gt lt uc groups decl gt lt local decls gt Predicate definition lt pred def gt value lt expr gt As for nodes zeroadic predicates i e without any input nor controllable sections are admitted 2 5 Variable Scope TODO Where variables can be used especially the local ones 3 Synthesizing using ReaX 3 1 Specifying a DCS Algorithm In order to compute a controller one first needs to select one of the synthesis algorithms available in ReaX and optionally provide additional options for it On the command line the algorithm descriptor can be specified as an string immediately following the a short version of a 1go flag Algorithm specific options can be set by appending a colon to the algorithm descriptor followed by a comma separated list of option flags or assignments and values for complex options e g lists of variables abstract domain descriptors must be enclosed in brackets For instance Algo flag option1l 42 option2 foo bar selects an algorithm Algo sets the a flag flag an option option to value 42 and option2 to a list of two strings Flags are considered disabled by default 3 2 Available Synthesis Algorithms ReaX currently implements two synthesis algorithms an ex
21. riginal node and its outputs are the two controllable inputs 11 2tasks ctrlf typedef S enum Idle Active input tle S7 t2 Sj rl bool r2 bool sl bool s2 bool clt Bool Soutput cl bool e2 bool local 10 bool 11 bool 123 bool 13 bool 14 bool 15 bool definition cl _cl 10 not rl 11 not r2 12 t2 Active 13 11 or 12 14 t1 Active or 13 15 10 or 14 c2 cl and 15 assertion true 3 5 2 Infinite state Case Example Node Consider an extended version of the previous example finite Controllable Nbac node now involving a numerical state variable In this model additional state variables x1 and x2 are used to count the number of steps spent in the Active state for each task Let 2tasks counters ctrln be the file 2tasks counters ctrin typedef S enum Idle Active state tly Ze Bi xl x2 int input rly r2 Sly B2y Cly 21 bool controllable ol 7 cel c2 uc2t bool 12 transition tl if t1 Idle and rl and cl then Active else if tl Active and sl or cl then Idle else t1 x1 if t1 Idle and rl and cl then 0 else if tl Active then x1 1 else xl t2 if t2 Idle and r2 and c2 then Active else if t2 Active and s2 or c2 then Idle else t2 x2 if t2 Idle and r2 and c2 then 0 else if t2 Active then x2 1 else x2 initial tl Idle and t2 Idle and x1
22. s execution in seconds Following are a character describing the log level E for errors W for warnings T for general information the default level and D d and for three further debugging levels Then comes the name of an internal module of ReaX and the payload itself 0 029 I Main Reading node from 2tasks ctrln 0 051 I Supra Variables bool num state 2 0 i 7 0 u 5 0 c 2 0 0 052 I Df2cf Preprocessing discrete program 0 052 I Synth Boolean synthesis 0 052 D sB y t1 Idle or tl Active and t2 Idle 0 052 I sB gt Invariance 0 052 I sB lt 0 052 D sB B t1 Active and t2 Active 0 053 I sB NB S2 true success 0 083 I sB Bullding controller 0 053 I sB Computing boundary transtions 0 053 I sB Simplifying controller 0 053 I Synth Boolean synthesis succeeded 0 055 I Env CUDD reordering 0 063 I t4 Triangulation 0 063 D t U C group i cl _cl c2 cl and not rl or cl and rl and not r2 and t1 Idle or cl and rl and r2 and t1 Idle and t2 Active or cl and rl and tl Active 0 064 I Main Extracting triangularized controller 0 064 I Main Checking triangularized controller 0 065 I Main Outputting into 2tasks ctrlf The resulting output file file 2tasks ctrlf encodes the triangulated controller Observe that its inputs are the union of all state and non controllable inputs of the o
23. tual exclusion between a list of Boolean expressions i e at most one can hold at a time and the membership test for finite types Semantics of the other constructs is straightforward 2 3 3 Type related Rules An optional section for type specifications always comes first in Controllable Nbac files Type definition section lt typdefs gt typedef lt typdecl gt Enuleration type declaration typdedcl is lt id gt enum side 1y lt i p TP y Type names lt type gt bool int real lt bint type gt lt id gt Bounded integers lt bint type gt uint sint lt positive gt 2 3 4 Variable Declarations Standard variable declarations are made using series of sets of identifiers associated to their type lt var decls gt lt var decls gt lt var decls gt i a tvar decls gt iis lt id gt lt td gt 2 lt type gt 2 3 5 Local Variable Declaration and Definitions Every category of Controllable Nbac input node function or predicate may use local variables to shorten or ease the specification of expressions Local variables are declared and defined in the 10ca1 and definition sections Declaration part lt local decls gt local lt var decls gt Definition part lt local defs gt definition lt local def gt lt local def gt F EE lt local def gt lt id gt lt expr gt A lo
Download Pdf Manuals
Related Search