Users`s and Programmer`s Manuals
Contents
1. f sigma includi bdd simplify control at PROGRAMMERS MANUAL C amp elig G sigma C amp elig Plant sigma all C amp elig Plant sigma Listing 2 2 Control function simplification Grammar of the Control Problem Model Syntax OMAN OO O WN EO O0 ARW NH A A A A BRI B amp BB WW WW WWW WWE NP N ND ND D NNP ND ND O U NEO ARA ND OH O0 JAR WN EE Control Problem Model Syntax Lexical elements Keywords AND OR EU Memory STu XO EBIT WEI Xm tBo STO STm WSN Delimiters Sis p 7 6 AL Tor Fr PE GR ORE RE ET id non empty string of alphanumeric characters beginning with an alphabetic character and such that it is not in Keywords qualified_id a string corresponding exactly to the pattern id id without any intervening white space character N B Identifiers are case sensitive ControlProblemDefinition STSDefinition STSDefinition CtrlSpecDefinition STSDefinition StateTreeDefinition StateTreeDefinition SpecialObjects StateTreeDefinition SuperStateDefinitionList SuperStateDefinitionList SuperStateDefinitionList SuperStateDefinition SuperStateDefinition SuperStateDefinition ANDStateDefinition ORStateDefinition ANDStateDefinition id AND StateExpansionDefinition ORStateDefinition id OR StateExpansionDefinition HolonDefinition2. S z ActiveStateSetList S rar rr rye ActiveStateSetList ActiveStateSetList ActiveStateSet ActiveStateSetList ActiveStateSet NameList Et Pope NameList UnqualifiedNameList NameList id Namelist qualified_id qualified_id UnqualifiedNameList UnqualifiedNameList id id MODEL SYNTAX oo 10 O WN EO O0 AAR O NH ee A A BRI BR B BR WW m W Q0 W Q2 EEN b ND ND ND ND PN ND ND ND NO AE NEO OO O WNEO O0 NIT AA O NHO Makefile of program stscps CC IN LI C I L BI Makefile of program stscps Makefile for the STS Control Problem Solver stscps First version completed 2012 04 16 Author Daniel C t from Universit de Sherbrooke ht Variable definitions Adjust the following to the appropriate distribution of gcc for the target machine Here the standard distribution of gnu c is assumed The application was designed under cygwin 2012 04 with the standard distribution of gcc which at the moment is gcc version 4 5 3 and uses the stdc v 6 0 library for STL among other things It requires a good version of the Standard Template Library STL the Buddy BDD package distribution buddy 2 4 tar gz from http sourceforge net projects buddy the Boost c libraries distribution version 1 33 1 or higher from http www boost org Only the shared ptr data type from the Boost libraries is used in the app
3. TMdlCompiler h CompilerDS h TAST h TSTS h TMdlSemantic h TState h TANDState h TORState h CompilerDS o CompilerDS h TState h TMdlSemantic o TMdlSemantic h TMdlParser h TAST h TAST o TAST h TState h Tokenizer o TTokenizer h TToken h TToken o TToken h TState o TState h TANDState o TANDState h TState h TORState o TORState h TState h cpp o CC INCL c cpp MdlParser o TMdlParser h TAST h TTokenizer h TToken h Bibliography 1 J Lind Nielsen BuDDy Binary Decision Diagram Package Release 2 2 IT University of Copenhagen ITU Copenhagen 2002 2 C Ma and W M Wonham Nonblocking Supervisory Control of State Tree Struc tures volume 317 of Lecture Notes in Control and Information Sciences Springer Verlag Berlin 2005 33
4. StateExpansionDefinition E UnqualifiedNameList HolonDefinition Memory HolonStructure HolonStructure HolonStructure InternalUncontrollableEventSet InitialStateSet InputBoundaryTransisionSet InternalTransitionSet TerminalStateSet OutputBoundaryTransisionSet 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 101 102 103 104 30 A GRAMMAR OF THE CONTROL PROBLEM InternalUncontrollableEventSet SIu z UnqualifiedNameList J ETU T ERI EET InitialStateSet xo UnqualifiedNameList InputBoundaryTransisionSet CBI z TransitionList InternalTransitionSet pu m rae opt tr Her Tr TransitionList TF TerminalStateSet Xm z UnqualifiedNameList OutputBoundaryTransisionSet LBO z TransitionList TransitionList TransitionList Transition Transition Transition Er id pd id tau id T gt SpecialObjects InitialConfigurationsDefinition TerminalConfigurationsDefinition InitialConfigurationsDefinition TerminalConfigurationsDefinition InitialConfigurationsDefinition STO z ActiveStateSet TerminalConfigurationsDefinition STm z ActiveStateSetList STm far f rye CtrlSpecDefinition
5. Template Libraries The program is also known to compile and run correctly on a sun system SunOS 5 10 using gcc3 with the compiler version gcc version 3 4 6 However version 6 0 of the libstdc libraries is important as the program may not work with prior versions 13 PROGRAMMERS MANUAL of that library Version 6 0 of libstdc represents a major re haul of the libraries relative to prior versions and that can be considered a real dependency for program stscps The program also depends on the following libraries e the Buddy BDD package version 2 4 from sourceforge http sourceforge net projects buddy e the Boost C libraries version 1 33 1 or higher http www boost org The dependency on the Boost C libraries is thin only one class is used shared ptr to implement a simple dynamic memory management scheme All data structures of program stscps have a clear hierarchical aggregation relationship amongst them So the shared ptr class from Boost is used to supply automatic dynamic memory management since it readily implements a reference counting scheme for dynamic memory management and takes care of releasing memory that is no longer used The dependency on the Buddy library is intrinsic for BDD usage 2 1 3 Functional Units and their Relationships There are three main functional units to the program 1 the application driver 2 the problem model 3 the model compilation instrumentation The application dr
6. basic state trees which are the target of a transition on event c This predicate can itself be obtained from the transition relation N embedded in Gamma by remov ing all the source i e primed variables from N through existential quantification Using buddy we have bdd N good Gamma nextG sigma amp C p 118 bdd f sigma Gamma N good sigma p 120 Note that only the deterministic case is covered here In particular as said in 2 at p 120 this definition of f only enables c at those system configurations that it has to This is important in the context of f simplification 2 2 3 Control Function Simplifications In 2 p 120 it is suggested that the control function i e the set of predicates f can be simplified using the bdd_simplify procedure of the Buddy BDD package What is suggested there is that under certain circumstances predicate f can be simplified by restricting its domain to C Eliga o where Eliga o is the eligi bility predicate of controllable event within the STS model However a further 25 PROGRAMMERS MANUAL example on p 122 clearly shows that there is more than one case involved and that the simplification predicate must vary in accordance to some set of criteria Unfor tunately a full rationale allowing to identify the useful cases and their corresponding simplification formulae is missing The following attempts to clarify that situation To begin with one can observe that rest
7. can be the labels of simple states in other struc tured states State labels in transition structures need not be qualified because of the relationship that must exist between structured states in ST The definition of ST is given as an active state set see 2 p 27 for the formal definition of active state set The definitions of STm and S are given as lists of active state sets The definitions of STo STm and S are all optional but when any combination of these three elements is present it must come after the definition of ST and it must follow the specific order S7o ST and S Any one of these can be omitted in a given control problem specification and the omitted elements are considered to be empty sets Omitting any or all of these elements will not prevent synthesis control problem resolution but may give rise to pathological situations since omitting ST for example makes all states of ST inaccessible and conversely omitting STm makes all states of ST non co accessible Active state sets are basically given as sets of state names In active state sets the name of simple states must be qualified with the name of their OR state parent This is necessary since simple state names are not registered at the global STS level and are not unique except within the scope of their OR state parent This is the only circumstance where it is necessary to use qualified names to uniquely identify states The names of structured states are nev
8. definition For this reason a limited form of name qualification is defined in the syntax for simple state names NP2 Simple state name can be qualified Only one level of qualification is necessary and allowed and the qualification operator is the dot for example A b Both qualifier id and qualified id names must be valid state names and the qualifier must be the name of the parent OR state of the qualified name Moreover only simple state names used in the definition of active state sets e g in order to define ST need and can be qualified oo oo O pP WN EO O0 RAR N H Q3 WW C9 Qo bh b b ND b b ND ND P N U N RFP ANDAR O NHO 1 2 CONTROL PROBLEM MODEL SYNTAX 1 2 2 Main Constructs of the Syntax A full example of a control problem model is given by Listing 1 2 This specification contains no error and generates no diagnostic It contains all four parts of a valid model e Lines 13 to 66 contain the definition of ST with the root defined as AND state x0 at line 13 to 16 e Line 77 is the definition of ST e Lines 82 to 84 is the definition of ST e Lines 91 to 94 is the control specification S The syntax allows both line comments and block comments Block comments can be embedded All names and keywords are case sensitive Listing 1 2 Example of a Control Problem Model Ma and Wonham LNCIS 317 2005 p 95 Fig 4 12 Example of an STS with a simple but non trivial vertical structure The S
9. progression function Gamma I in 2 is declared and implemented as an internal compiler data structure in module CompilerDS cpp because it has internal state in the form of a set of transition relations entities N in 2 Module TSTS cpp and CompilerDS cpp are the modules that interface and use the BDD package other modules do not 2 1 6 Tokens and the Tokenizer Most of the logic to identify extract and classify tokens from the input stream is part of the TToken class Most of its routines are inline routines and the structure itself is constant The source code should stand on its own and is straightforward There are primarily two token classes identifiers and delimiters Identifiers are defined as case sensitive alphanumeric strings beginning with an alphabetic character Delimiters are special characters with specific meaning such as and to name a few Delimiters are further sub classified as keywords as are also a certain number of reserved identifiers such as STO STm among others An exhaustive list of keywords and 16 2 1 SOFTWARE ARCHITECTURE OF THE STSCPS PROGRAM token classes can be retrieved from the class implementation TToken cpp where they are listed in tables There are three special token types One the eos for end of stream token is there for the tokenizer to be able to recognize the end of the input stream A second one the error token is there to be returned by the tokenizer to the parser when
10. set of classes used for run time representation of ST TState TORState and TANDState in corresponding source modules Predicate representation however requires special data structures Apart from the fact that the compiler should not be too tightly coupled with the BDD package in case the program is eventually ported to other BDD packages the BDD package is not operational during compilation hence direct BDD encoding of the predicates is ruled out The data structures provided by the compiler must contain all the 20 2 1 SOFTWARE ARCHITECTURE OF THE STSCPS PROGRAM information necessary for the BDD package to produce correct BDD encodings of the predicates at a latter phase In the STS framework predicates are used mainly for two purposes 1 as characteristic functions identified with state sets see section 4 2 1 of 2 2 to express transition relations in the STS see section 4 2 1 of 2 In their simplest expression apart from the constants true and false such predicates express variable bindings of the form v qo or v qo q1 where x is the label of an OR state and identifiers such as go are the labels of states within the holon matched to x This kind of predicate that use a single variable is enough to express characteristic functions of state sets However to express a transition inside a holon both the source and target states of the transition must be expressed which requires a second variable As a co
11. specification only one of the two can be specified The same relationship exists between X and the boundary output transition set go This rule is consequent to the definition of holon given in section 2 2 of 2 Basically if an OR state s holon expands a parent holon see 2 p 39 to get a definition of expands then dg and go are generally not 9 Oo O O NH HH USER S MANUAL Example of a memory element meml OR State direct expansion E q0 al Matched holon Memory SIu mu tBI q0 tI lt q0 beta ql gt lt ql mu q0 gt tBO q0 Listing 1 3 Example of a memory element empty and their contents completely define X and X respectively However when an OR state is AND adjacent to the root its external structure is empty and both dpr and dgo are then empty In that last case e g x1 and x2 in Listing 1 2 the contents of xo and xm should be given explicitly by the user since these sets cannot be empty Transition sets are made of three tuples of comma separated labels enclosed by angle brackets each representing a transition e g line 53 in Listing 1 2 Their structure is source state label event target state label Internal transi tions tr source and target states must be in the state s expansion Boundary Input transition sources must refer to external states as well as target states of Boundary Output transitions External states
12. the text of the input stream does not match any token class The error token always contain an error diagnostic information attribute to allow the parser to issue a more meaningful diagnostic than a bland unrecognized token kind of message Finally the nat or not a token token if ever returned by the tokenizer signals a logic error in the tokenizer itself The source code for class TToken should stand on its own and is really pretty straightforward The TTokenizer class implements a simple straightforward tokenizer It manages the input stream breaking it in tokens bypassing comments and illegal characters within it The tokenizer has an explicit command to acquire the next token in the input stream the nextToken command The tokenizer automatically recognizes and bypass line comments block comments and illegal characters that are present in the input stream as part of its nextToken acquisition logic Block comments can be embedded Apart from the logic for bypassing comments and illegal characters the tokenizer keeps a copy of the last token that has been extracted from the input stream the current token This current token can be queried for a match on its type or on its text the 1ookup queries 2 1 7 The Model Parser The parser uses the tokenizer to read an input file the model of a control problem and produces five objects as result of the parse 1 a map containing the state descriptors of the list of structured
13. the operators for conjunction disjunction and negation are used In particular func tions TSTS supC2P TSTS CR and TSTS Bracket closely follow their formal definitions in 2 respectively supC P CR G and I Other interesting instances of the use of the BDD package can be found in source module CompilerDS cpp For example the translation of a basic Simple expression ie a variable bindings expression is illustrated in Listing 2 1 Note that at line 5 the fdd domain variable number is copied into var This variable number is used for all variable values of the variable bindings expression At line 9 a value for the variable var is copied into val and at line 11 a predicate for the variable binding var val is computed with bdd ithvar var val Finally it is combined with previous variable bindings if any through disjunction operator 0 Notice that the result of bdd_ithvar var val is an encoding of a prediacte of the form v val provided that var contains the BDD variable number corresponding to OR state x If the Simple expression contained more than one variable bindinds then the effect of method TPPSimpleExpr eval above is an encoding of a predicate of the form v 24 2 2 SPECIAL SUBJECTS Finally the most complex use of the BDD package can be seen in source module CompilerDS cpp in the definition of the data structure corresponding to Gamma Gamma is defined as a data stru
14. C Eliga o is at least as strong as fo then o is allowed to happen as soon as it is eligible within C the control problem solution space This condition means that within the confines of the control problem solution space Eliga o itself is adequate as a control function because then all control over the occurrences of is exercised exclusively by explicit constraints expressed in memory elements of the STS Under that circumstance the simplest expression of the control exercised by the system is the restriction of Eliga o not fs to C P where P Eligprant o This factors out CA Eligprant o from Eliga o leaving only the factors involved in explicit control constraints Fortunately this condition is easy to test since when CA Eliga o lt fo then CA Eliga oa f C Eliga o Finally following this overall rationale a general procedure given in Listing 2 2 can be devised for the simplification of the set of predicates f The algorithm of Listing 2 2 assumes the usage of Buddy and also f such as calculated previously and C the predicate identified with the control problem solution space 27 0 NI Oo O B amp OV NH m o bdd elig G sigma or bdd elig Plant sigma bdd f sigma opt if Explicit f sigma opt else All other f sigma opt f sigma amp ontrol cases bdd false C amp elig G sigma only bdd simplify elig G sigma within C no explicit
15. State Tree Structures TMdlParser cpp Implements the concrete syntax parser for control problem models cf Appendix A TAST cpp This module define all the data structures used to represent the abstract syntax corresponding to Appendix A This module also defines more than one data type T Tokenizer cpp Implements a simple tokenizer for use with the parser TToken cpp Implements the token representation TANDState cpp Implements the representation of AND super states a runtime data structure TORState cpp Implements the representation of OR super states a runtime data structure TState cpp Implements an abstract class representing structured states a runtime data structure The build Makefile given in Appendix B compiles and assembles them into an application As a rule one source code module usually defines a single data type or a small set of tightly coupled data types Exception to that rule are the source modules CompilerDS cpp and TAST cpp Most data types are prefixed with the capital letter T as in class TMdlCompiler This is done for quick recognition in source code inspections Most of the attributes and method names follow the usual naming con vention of C Attributes are prefixed with a lower case f for field e g attribute fSemanticChecker Names are usually written in lower case with a capital letter at the beginning of each word except for the first word e g method listParentChild There are
16. TS itself is not interesting for a Control Problem specification but in terms of STS structure it covers most of the non trivial cases and is simple enough that one can visually check the data structures resulting from its compilation kkk k k k k k k k k Definition of ST x k x k ko x ke k ST root state xO AND State direct expansion E xl x2 OR Superstate bl b1 OR State direct expansion E b10 bil Matched holon SIu mu tBI lt a alpha b10 gt tI lt b10 mu bil gt tBO lt b11 beta c gt OR Superstate b2 b2 OR State direct expansion E b20 b21 Matched holon SIu tBI lt a alpha b20 gt USER S MANUAL EI lt b20 lambda b21 gt tBO lt b21 beta c gt OR Superstate b b AND State direct expansion E bl b2 OR Superstate xl xl OR State direct expansion E abe Matched holon SIu beta xO a a tI lt a alpha b gt lt b beta c gt lt c alpha a gt xm a OR Superstate x2 x2 OR State direct expansion E de Matched holon SIu beta X0 d d tI lt d beta e gt lt e sigma d gt Xn d d kkkk k k k k x x x Definition of STO and STM xxx kk ok kk x k k k kk ke ke ke x x Initial configuration of the STS given as an active state set N B In active state se
17. The STS Control Problem Solver Program stscps User s and Programmer s Manuals Daniel C t et Richard St Denis Departement d informatique Universit de Sherbrooke May 7 2012 We want to thank Mr Benoit Fraikin from the Departement d informatique de l Universit de Sherbrooke for providing the main EITRX package used to typeset this brochure and more generally for his assistance in matters of typesetting with IATEX ii Contents 1 User s Manual LL Programi dE ee BES ee 49 RUE Ee HE bare S 1 2 Control Problem Model Syntax e e eene een 1 2 1 Syntactic Assumptions and Inference Rules 1 2 2 Main Constructs ofthe Syntax 1 2 3 Results Interpretation 22r 2 Programmers Manual 2 1 Software Architecture of the stscps Program 2 1 1 Van Documentation oz gt e ace 2 die we ee we 212 Build Enyironment e wa sa ee RE E as 2 1 3 Functional Units and their Relationships 214 TheApplicationDriv r Er Tel can a Ow Re Pee ee hy ter ces 2 1 6 Tokens and the Tokenizer alt The Model PRESE 29e Lea ee ri part ec 2 1 8 The Semantic Checker 21 9 The Model Compiler 2 2 4 22 56428 ep eben x 2 2 Dpecial Subjects gt e a eea au e Be a a a 2 2 1 Finite Domain Predicates Using Buddy 2 2 2 Computations of Control Predicates 2 2 3 Control Function Simplificatio
18. also exceptions for that rule primarily with respect to names of formal 15 PROGRAMMERS MANUAL entities defined in 2 for example function Gamma function cR and function supC2P The program was coded with the goal that functional objects and formal entities defined in 2 should be recognizable as such in the source code as much as possible 2 1 4 The Application Driver The code for that module should stand for itself and is indeed quite simple As mentioned previously the application driver basically analyses the command line for consistency then eventually instantiates a control problem and solves it 2 1 5 The STS The data type TsTS is a class that represents the model of an STS In fact in the current version of stscps TSTS represents a control problem model because it contains the control specification Ps Properly speaking there should be another class to represent a control problem model of which the STS would be an attribute However synthesis is very tightly coupled with the STS through the definition of Gamma the reverse progression function so that isolating STS and control problem model in two different data types would have required gymnastics that would have obscured the logic Most of the functional entities required for synthesis are defined within the TSTS class In particular the operators supc2P operator supC P in 2 Bracket operator in 2 and cR O0 operator CR G in 2 The reverse
19. cture because it has state in the form of a set of transition relations N As a result Gamma is an object and redefines its operator with the specific signature of T P o The text of TGamma operator contains the most complex examples of the use of the BDD package Gamma requires existential quantification bdd exist over variable sets not only single variables The function used to obtain variable sets with Buddy is fdd makeset that takes a table of variable numbers as input Also Gamma requires variable replacement bad replace which in turn requires that sets of paired vari ables be made through a call to fdd_setpairs that takes two sets of variables to be paired as input typically primed and normal variables will be paired for re placement with one another Pairs must be stored in special BDD package data structures called badPair allocated through a call to bdd_newpair and deallocated through a call to bdd_freepair Finally routines bdd_true and bdd_false are also used to get the special constants bdd True and bddFalse respectively And shutting down the BDD package is effected through a call to routine bdd_done 2 2 2 Computations of Control Predicates The un simplified control predicates are obtained from the definitions for the deter ministic case at pp 118 120 of 2 There predicate Na is specific to a particular event c and is calculated from predicate Nexta c the predicate identified with all
20. domain variable for us the variable associated with an OR state Buddy allocates log2 p basic BDD variables where p is the number of values in the domain of the variable for us the number of states of the holon matched to the OR state Of course that means that for a domain of 17 values five BDD variables are required to represent the values 0 16 and the values 17 31 are not really used and should not appear in predicates for that finite domain variable However values 17 31 may appear particularly as a result of predicates negation Such a fact will not alter the results of synthesis but will make reading the results of synthesis a bit harder The program uses a very little sub set of the routines of the BDD package Initial ization of the BDD package must occur first and uses the bdd_init routine called with appropriate parameters Immediately after initialization finite domain variables must be allocated using the int bdd_extdomain int domain_sizes int array_size routine This rou tine can allocate more than one finite domain variable in a single call That is the reason for the domain_sizes array parameter This array must contain the sizes of the domain variables being allocated This corresponds to the parameter p of D 0 1 p 1 for a specific domain variable The parameter array size is the number of finite domain variables to be allocated The function returns the variable numbers of the domain variables T
21. e program can compute a solution to the control problem and printing that solution is never suppressed 2 1 2 CONTROL PROBLEM MODEL SYNTAX BDD package run time options are supplied here only to try to isolate the user from the complexities of configuring the package The Buddy BDD package requires mainly that a user supplies at least the BDD node table size at package start up time routine bad init of the package Heuristic rules are given to size the cache tables relative to the BDD node table size and other parameters all have a default behavior Therefore BDD options concern mainly BDD node table size e Option bddsmall corresponds to a BDD node table size of 214 nodes e Option badMedium corresponds to a BDD node table size of 2 nodes e Option badLarge corresponds to a BDD node table size of 2 nodes e Option bddBig corresponds to a BDD node table size of 224 nodes The default BDD node table size corresponds to option baddMedium Each BDD node in Buddy takes up 20 octets of space so that the default requires about 2 5 Mb of dynamic memory plus about 1096 of that for cache memory There is also an option bad int taking an integer parameter n in the range 14 lt n lt 24 representing a power of 2 used to calculate the size of the BDD node table so that bad 17 gives the same result as bddMedium i e a BDD node table size of 2 nodes 1 2 Control Problem Model Syntax According to 2 abstractly a cont
22. er qualified they must be always be 10 D e oo oo N H 0 oa O W 1 2 CONTROL PROBLEM MODEL SYNTAX stscps Tests test mdl PS lt x1 0 gt C cupC2P PS x1 2 x1 1 PO amp C xl 1 bl1 0 b2 0 x2 0 gt Non optimized solution f alpha x1 0 f lambda x1 1 b2 0 F sigma xl 2 x2 1 x1 1 x2 1 Optimized solution f alpha F f lambda T f sigma T Listing 1 4 Example of a control problem resolution unqualified identifiers even in active state sets 1 2 8 Results Interpretation The resolution for the problem model given in Listing 1 2 is given on Listing 1 4 The command line line 1 invokes stscps with the appropriate model file with all default options compile level So1ve output detail level silent and badMedium BDD node table size The results produced are predicates which are printed by the BDD package itself e PS stands for the predicate identified with the control specification Ps the family of forbidden configurations of the STS e c stands for the control or synthesis predicate C supC P Ps e PO amp C stands for Py C the predicate identified with the family of allowable initial system configurations under C The other predicates represent the control function in non optimized form raw pred icates such as calculated by the synthesis procedure and optimized form simplified predicates such as in
23. escriptor identifies the state itself and its type All structured states have an expansion introduced by the keyword E which is formed of an ordered set of labels A state s expansion can contain labels of other structured states e g xo an AND state lines 13 to 16 refers to OR states x1 and x2 Note that the expansion of a state may contain the labels of simple states as for OR state b1 at lines 19 to 27 structured state labels as for x0 or a mixture of both as for OR state x1 at lines 47 to 55 For AND states the expansion is the only element of internal structure For OR states the expansion must be followed by a description of their matched holon see for example OR state b1 at lines 23 to 26 and contrast it to OR state x1 at lines 51 to 54 A holon description can start with the keyword Memory to indicate that it is the holon of a memory element e g Listing 1 3 If this is the case the keyword Memory must be the first element of the holon description The other elements are SIu standing for Xj the uncontrollable internal event set XO standing for Xo the initial state set tBI standing for p the Boundary Input transition set tI standing for 6 the internal transition set tBO standing for 080 the Boundary Output transition set Xm standing for X the terminal state set Note that the syntax precludes specifying both the initial state set Xo and the boundary input transition set dg together within the same holon
24. essage and abort the parse otherwise do whatever is required and go to the next token 3 go back to step 1 until no more token is expected and the end of the input stream has been reached Of course that takes the form of linear procedures and procedure calls to keep track of progression in the text of different constructs The hardest part is the necessity of giving the best possible parse error message on syntax error detection Apart from syntax error detection the parser also detects static consistency error and diagnostic or warning conditions On consistency error detection the parser issues an error message but the parsing process is not terminated if no syntax error is present Also some diagnostic conditions must be signalled but do not require terminating the parse as they may not be error as such e g a duplicate state name declaration in the expansion of a structured state When a diagnostic condition arises the parser issues a warning message and undertake a recovery action to correct the condition the parsing process is not terminated The parser can be interrogated by the semantic checker a friend class as to the result of the parse As a debug facility all data structures from module TAST cpp can be printed to see if the results of the parsing process are as expected The parser can print a parse summary and a listing of the source of the model file depending on options given to it in its constructor Parse error diagn
25. hese variable numbers are referred to as BDD variables in subsection 2 1 9 the compiler section These variable numbers are very important They are the variable numbers that must be used for reference variable number resolution As such they are collected in the map fv2BDD of the TSTS class 23 oo Ct WN H PEPER a U N H PROGRAMMERS MANUAL bdd TPPSimpleExpr eval bdd result bdd_false TVarBinds amp simple_expr fSimpleExpr index_t var simple_expr 0 for int i 1 i lt simple_expr size i index_t val simple_expr i result result fdd_ithvar var val return result Listing 2 1 Simple expression BDD encoding which map reference variable numbers primed and normal variables onto BDD or more accurately fdd variables assigned by the BDD package Orderly call to bad_init and bdd_extdomain are both performed by method STS startBDD If the BDD package did not return any error during the call to STS startBDD then the BDD package has been successfully started all Pseudo Predicate variables have been resolved and the model is ready for synthesis Other wise if the BDD package refused to start for some reason then the BDD package has been orderly stopped and is not working and variable resolution has been canceled and all variables restored to their original reference variable values Some other uses of the BDD package can be seen in the Tsts class where mostly
26. icient conditions given in p 57 of 2 for the soundness of function A As part of this verification process some attributes of the state descriptors are calcu lated in preparation for the compile phase 2 1 9 The Model Compiler The model compiler class TMdicompiler plays a pivotal role in the compilation process As mentioned previously it isolates class TSTS the real problem solver class from the parsing and consistency verification As a result a characteristic of class TMdlCompiler is that it shares most of its attributes with other classes This is a design decision that may be challenged but it was taken in order to minimise the copying of data structures around The model compiler receives the AST data structures source module TAST cpp h from the parsing and semantic verification phases and starting from these computes a set of run time data structures that it hands over to the TsTS class Those run time 19 PROGRAMMERS MANUAL data structures are defined in source code modules CompilerDS cpp h TState cpp h TORState cpp h and TANDState cpp h Here the term run time data structures only means that the set of data structures used during control problem resolution is a lightweight version of those produced as a result of model parsing This is due to a design decision made on the basis that BDDs are potentially memory hungry data structures In order to reduce memory consumption during control problem resolution where it is
27. is diagnosed as redundant and ignored The parser issues a warning to that effect but continues parsing However the user cannot receive any warning about a mis spelling on the name of a structured state In order to make control problem models as compact as possible the definition of ST has been extended to include holon definitions as part of the definition of the OR super state to which they are matched Most information about the structure of a holon is comprised within its transition relation The transition relation of a holon is partitioned in three transition sets the boundary input boundary output and internal transition sets From these the parser can recover most of the other elements of the holon structure by making the following assumptions A1 All states that are either source or target of an internal transition are assumed to be part of Xz the internal state set of the holon A2 All targets of boundary input transitions are assumed to be part of Xo the initial state set of the holon A3 All sources of boundary output transitions are assumed to be part of X the terminal state set of the holon A4 The entire content of Xo U X is assumed to be a subset of Xz the internal state set of the holon A5 All sources of boundary input transitions are assumed to be part of Xp the external state set of the holon USER S MANUAL A6 All targets of boundary output transitions are assumed to be part of Xz the external state
28. iver basically analyses the command line for consistency then eventually instantiates a control problem and solves it The control problem uses the model compilation instrumentation in order to load the textual representation of the control problem model and transform it into data structures suitable for problem resolution Then the control problem model can apply the procedures of to obtain a solution and list it on the console The project comprises twelve source code modules AppDrv cpp Implements the application driver TSTS cpp Represents the control problem model and implements the problem res olution routines The rest of the modules implement the compilation instrumentation Their function is to build a control problem representation that is suitable for the problem resolution procedures implemented by TSTS cpp 14 2 1 SOFTWARE ARCHITECTURE OF THE STSCPS PROGRAM TMdlCompiler cpp Implements the control problem model compiler It is a cen tral class that plays the role of interface between the rest of the compilation instrumentation and the control problem model TSTS cpp CompilerDS cpp This modules defines most ofthe runtime data structures involved in problem resolution Contrary to other source code modules this module defines more than one data type TMdlSemantic cpp This module implements the semantic verification logic of the compilation process It mainly verifies the properties defined in 2 for State Trees and
29. lication to implement a simple dynamic memory management scheme i e hierarchical data structure containment with reference counting C CL I usr local include BS L usr local lib lbdd lstdc The following works on host mirka dmi usherb ca for the gcc4 distribution To compile using gcc 4 on that host comment the previous definitions and uncomment the following definitions C opt csw gcc4 bin c NCL I usr local include I opt csw include IBS L usr local lib lbdd lstdc Object code modules NS AppDrv o T T C T T STS 0 MdlCompiler o ompilerDS o MdlSemantic o MdlParser o 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 101 102 103 104 105 106 32 TAST o TTokenizer o TToken o TANDState o TORState o TState o ht Target definitions all stscps ls al stscps test stscps stscps Tests test mdl Compile Verbose SFltest stscps stscps Tests SFl mdl Summary TLtest stscps stscps Tests TL mdl Summary stscps BINS CC o stscps BINS LIBS clean rm f x o stscps stscps exe stackdump core AppDrv o AppDrv h TSTS h B MAKEFILE OF PROGRAM STSCPS TSTS o TSTS h TMdlCompiler h CompilerDS h TMdlSemantic h TState h TANDState h TORState h TMdlCompiler o
30. n the eligibility of c Then by definition Eliga o gt Eligpiant o The practical value of this definition of Eligpiant is that it is always safe and sound to simplify f by restricting it to CAP where P Eligpiant 0 The rationale is the same as in the RW framework an event cannot occur in the controlled system unless it is eligible in the Plant meaning that the system s current configuration b satisfies Eligpiant o This restriction factors out Eligpiant o from f thus simplifying its expression It should be mentioned that this simplification of f covers the case illustrated on p 121 for control function fi This may not be obvious at first glance since the suggested simplification predicate is C Eliga o However it should be obvious that when an STS model contains no explicit constraint on a controllable event c then Eliga o is the same as Eligpiant o since no memory element of the STS is involved in the eligibility of o This is the situation that prevails at p 121 of 2 for control function f More generally it can be true that CA Eliga o is the same as CA Eligprant o even if Eliga o lt Eligprant 0 in the STS model at large However it is not necessary to test for that specific condition since a simplification on P Eligpiant o is always sound and safe The only thing that can happen is that this simplification may not deliver the simplest expression for fo On the other end of that spectrum when
31. n the software architecture of stscps and other subjects useful for someone intending to modify the source code of stscps 2 1 Software Architecture of the stscps Program 2 1 1 Useful Documentation The documentation on the Buddy 2 4 BDD package can be found in PS format in the doc subfolder of the standard distribution of the package The main doc ument is 1 The Buddy 2 4 BDD package distribution can itself be found at http sourceforge net projects buddy The documentation on the GNU implementation of the STL libraries libstdc version 6 0 can be found at http gec gnu org onlinedocs libstde latest doxygen but a more usable documentation set can be found at http www cplusplus com reference The documentation on the Boost C libraries can be found at http www boost org The documentation on the shared_ptr class is part of the Smart Pointers module documentation Apart from that as mentioned before 2 is the main reference for everything concerning the supervisory control of STS 2 1 2 Build Environment Program stscps has been coded in the cygwin environment from red hat on the PC of the Reactive Systems Lab of the Universit amp de Sherbrooke 2012 04 The distribution of the cygwin environment used was current at the time and the installation was the default one adding gcc compilers and tools The version of the compiler is gcc version 4 5 3 GCC using libstdc v 6 0 for the STL C libraries Standard
32. necessary to use BDDs it has been decided to tightly isolate parsing from control problem resolution After successful parsing and semantic checking have been achieved the compiler must take the resulting model and produce an entirely different set of data structures that are compact and tailor made to allow the efficient encoding of the control problem into a form that can be used to solve the problem with BDDs Once the compiler has performed this task the compile phase terminates destroying all data structures related to the AST leaving only the so called run time data structures Then and not before the BDD package can be initialized and used for control problem resolution From chapters 3 and 4 of 7 it is possible to gather what are the required entities for control problem resolution 1 the tree structure of ST 2 a predicate encoding i e BDD encodings of T the reverse transition rela tion of the STS 3 predicate encodings Po Pm and Ps respectively for STo ST and S The tree structure of ST need not be complete at control problem resolution time e The containment information is required so the expansion of the structured states must be explicit e OR states need to add events alphabet and uncontrollable event set informa tion e Whereas AND states need to add child states clustering information see p 108 of 2 definition 4 4 for information on the notion of clusters That explains the form of the
33. ns A Grammar of the Control Problem Model Syntax B Makefile of program stscps PN S Q H HM 13 13 13 14 16 16 16 17 19 19 22 22 25 25 29 31 iii CONTENTS User s Manual The STS Control Problem Solver stscps is a program that performs the resolution of control problems specified using the STS modeling framework The main reference for the user s and programmer s manuals with respect to the STS framework is 2 which introduced the nonblocking control of State Tree Structures as a major variant of Supervisory Control Theory SCT 1 1 Program Usage The program is invoked at the command line and requires as a parameter a valid Control Problem Model file The model file is first parsed to verify that its contents defines a valid Control Problem Model Most of these verifications center around the properties of well formed STS given at section 2 3 of 2 If the model file contains a valid Control Problem Model then the program proceeds to apply the synthesis procedures exposed in chapters 3 and 4 of 2 to compute a State Feedback Control Law as a set of predicates f one for each controllable event c of the STS The main output of the program is the set of control predicates f which are simply printed out on the console If the command line invocation of the program is incorrect a short error message is printed Listing 1 1 below along with a summary of the program command line u
34. nsequence OR states must be assigned two variables one called the normal variable and the second called the primed variable Most predicates including characteristic functions of state sets are defined over normal variables only Transition relations are defined over both primed and normal variables Most BDD packages and Buddy in particular identify BDD variables by integer indexes Since at compile time BDD variable numbers are not known because the BDD package is not operational a data structure must be supplied to allow keeping track of BDD variable numbers once they are assigned by the BDD package at problem resolution time run time For that purpose OR states in ST are assigned an index at compile time The order of compile time index assignment is more or less arbitrary Here indexes are assigned in depth first pre order From the compile time OR state index a reference position for the two variables of a node primed and normal can be calculated according to the following formulae primedVar i 2 i normalVar i 2xi 1 The reference indexes can thereafter be used to index a table mapping reference variable numbers to BDD variable numbers That process is called variable resolution and occur in class TSTS as an initialization of the BDD package Variable resolution consists of scanning data structures prepared by the compiler and replacing each occurrence of a reference index by the actual BDD variable number computed at BDD
35. of the compilation gives a summary of its operation and they enable the source code of the model file to be listed along with the diagnostics of the parser the semantic checker and the model compiler The default option for that category is Solve which assumes that the Control Problem Model is valid and suppresses as much output as possible by assuming output detail option Silent Note that any error or diagnostic generated during compilation will always be printed during the compilation phase no matter the compile level or the output detail level requested Using compilation level of solve if the compilation generates no error and no diagnostic the compilation generates no output Output detail level options behave as follow e Option Silent suppresses as much output as possible during compilation If no error and no diagnostic are generated during compilation then compilation is silent generates no output However compilation errors or diagnostics are never suppressed e Option Summary prints summaries for all phases of the compilation process parsing semantic checks and compilation proper e Option verboseis really only a debugging facility for programmers to perform diagnostic or maintenance on the program With the verbose option all internal data structures of each phase of the compilation are printed along with the summaries for each phase Of course if the Control Problem Model is error and diagnostic free then th
36. ostics and consistency error messages are printed on stderr in C cerr No matter what the parse options are none of the error and diagnostic messages printed by the parser can be suppressed an incorrect model always results in error messages or diagnostics being printed 18 2 1 SOFTWARE ARCHITECTURE OF THE STSCPS PROGRAM 2 1 8 The Semantic Checker The semantic checker class TMdlSemantic takes the AST such as defined in the parser section subsection 2 1 7 and applies different tests to it in order to verify that it conforms to properties given in 2 1 The model is first verified to form a tree structure from the presumed root involving all states of the model This tree structure is verified to be well formed as defined in 2 definition 2 2 pp 14 15 2 Holons matching properties such as defined in 2 definition 2 14 pp 35 36 are then verified 3 Holons boundary consistency properties pp 38 39 are also verified 4 The model is also verified to obey the local coupling rule definition 2 16 of 2 pp 40 41 5 The STS is verified to be deterministic as part of the parsing process and this property is assumed by the semantic checker if the parser completes without any consistency error 6 Holons sharing events among them are verified to agree on the controllability status of shared events 7 In order to insure the consistency of the transition relation of the STS the model is verified to fulfill the suff
37. pp 120 122 Predicate computation and optimization or simplification is detailed in subsection 2 2 2 The BDD package provides a way to print variable names instead of their numeric IDs in printed results One can see in Listing 1 4 that for example Ps is given by the term x1 0 which represents an assignment of value 0 to variable x1 Of course 11 USER S MANUAL variable x1 stands for its namesake at line 47 of Listing 1 2 but the value 0 does not correspond to any value of the expansion of state x1 which are given at line 49 of Listing 1 2 E a b c This is because the BDD package does not provide for registering symbolic names for variable values Values are encoded starting from index 0 and following the same order as in the expansion For E a b c a gets the index 0 b gets the index 1 and c gets the index 2 The reader must do the translation himself Apart from that any variable bindings in a list between and stand for a conjunction For example PO amp C x1 1 b1 0 b2 0 x2 0 means P AC 2 1 by 0 by 0 zs 0 Two or more terms on the same variable such as in C cupC2P PS x1 2 x1 1 stand for C supC P Ps x 1 2 This is a little inconvenient to read but in order to do better one would have to massage the BDD package results significantly which is not a trivial task 12 Programmers Manual This section contains notes o
38. ricting f to C the control problem solution space predicate is always a sound and safe default strategy Effectively when the controlled system is started from a valid configuration b CAP no configuration b C should ever be reached while the controlled system is in operation If ever such a configuration was reached it would mean that something has gone wrong either with the equipment of the system or with the models that were originally used for synthesis Restricting f to C means that the controlled system disables c for all configurations b E C which is a safe default strategy This suggest that the general form of the simplification predicate is C P where P is an event eligibility predicate of some kind However the suggestion made on p 120 P Eliga o is clearly based on a special case and cannot be relied upon to be adequate in all cases as is also clearly illustrated on p 122 For an STS model event eligibility can be defined by Eligg c such as given in 2 pp 47 48 This definition considers the eligibility of event o involving all holons of the STS model including all memory elements holons Therefore Eliga o contains all control constraints on o which are explicit in memory elements of the STS model Explicit constraints on controllable events still require the control function to enforce them it would be unsafe to factor them out of the control function while simplifying it In the RW framework there exist
39. rol problem is fully specified by the two following objects 1 the definition of an STS 2 the definition of S a set of forbidden state trees for the STS called the control problem specification The STS definition is in turn made of six objects 1 a set of holons H an alphabet X and a forward transition function A 2 the definition of ST the state tree describing the structure of the state space of the STS 3 the definition of S7Tn the set of initial configurations of the STS 4 the definition of STm the set of final configurations of the STS USER S MANUAL Each OR state of ST must be matched to one and only one the holons in H By extending the definition of ST with a description of the holon matched to everyone of its OR states as part of the OR state description the elements of H X and A can be recovered from the extended definition of ST Consequently in the syntax adopted here for the specification of control problems a complete specification is therefore made of the following four elements 1 the definition of ST 2 the definition ST 3 the definition of ST 4 the definition of S In the proposed syntax a control problem definition must follow that specific order The details of the proposed syntax for Control Problem Models are given in the grammar at Appendix A What follows is a high level summary of it 1 2 1 Syntactic Assumptions and Inference Rules In a Control Problem Model the defini
40. rticular the names of simple states must be unique within the scope of their parent s direct expansion to distinguish between the children of the super state But beyond that it is often meaningless and cumbersome to distinguish 4 1 2 CONTROL PROBLEM MODEL SYNTAX between two simple states that already belong different parents Indeed one is often tempted to re use the same simple state names for different parents super states particularly when these names do not have any specific meaning e g q0 q1 There is however reasonable ground for assigning unique names to structured states i e names that are unique across the entire scope of an STS Since OR super states are assigned variables for synthesis expressing the results of synthesis using the name of the corresponding OR super states often makes those results more human readable Besides structured states are usually scarcer than simple states in an STS and often have system wide significance Consequent to that the following naming policy has been adopted and a related inference rule is followed by the parser NP1 Structured states must be assigned names identifiers that are unique system wide across the entire scope of the STS I1 Any state name that is not registered system wide as the name of a structured state is inferred to be the name of a simple state As a consequence of this inference rule any structured state definition bearing the same name as a previous one
41. s another definition of event eligibility that con siders event eligibility in the free uncontrolled behavior of something called the Plant There memory is not modeled explicitly What are modeled instead of mem ory elements are control constraints Therefore within the RW framework event eligibility is relative to Plant components and Plant components are loosely de fined as any specification element that does not model a control constraint This notion of event eligibility call it Eligpiant o is very useful since Plant components sharing events are assumed to synchronize on shared events without the intervention of the control function As a result since an event c cannot occur in a controlled system unless it is eligible in the Plant the expression of a control function such as fo never needs to contain Eligprant o explicitly in its formulation This is exactly the form of simplification that is sought for the STS control functions Both STS mem ory elements and RW control constraints have much in common and even though there is no notion such as the Plant in the STS framework a definition analogous to Eligpiant o can be developed starting from the definition given for Eliga o in 2 by disregarding STS memory elements in the definition Using the definition of Eliga o define Eligpiant o for an STS model where 26 2 2 SPECIAL SUBJECTS Eligpiant o disregards the effect of memory elements o
42. sage 1 stscps 2 To few arguments 3 Usage is 4 stscps file name stdin options 5 6 When using stdin the source model must be piped in instead of giving a 7 file name 8 Options 9 Parse Semantic Compile Solve control the compilation level 10 default is Solve 11 Silent Summary Verbose control the amount of details given 12 during compile default is Silent bddSmall bddMedium bddLarge bddBig control the size of the bdd package node table default is bddMedium Also bdd n where n is an integer power of two in the range 14 24 can be used H aa RO Listing 1 1 stscps program command line USER S MANUAL The program requires the name of a file containing a Control Problem Model and can take a few options Option stdin allows the user to pipe in the Model file instead of giving its name as an argument The other options are divided in three categories e compile level control options e output detail level control options e BDD package run time options Compile level control options Parse Semantic and Compile control the compilation level They are intended to provide assistance to a user that is designing a Control Problem Model while this model still contains errors syntax or consistency errors They can be seen as model debugging options In particular they will automat ically enable the Summary output detail level so that each phase
43. set of the holon A7 All events labeling internal transitions are assumed to be part of X the internal event set of the holon A8 All events labeling boundary transitions input or output are assumed to be part of Xp the external event set of the holon The only structural element of a holon that cannot be recovered from its transition relation is the partition of its internal event set in controllable and uncontrollable events For that reason the syntax requires the user to supply the list of internal uncontrollable events of the holon which of course are assumed to be part of the internal event set of the holon assumption A9 The parser then makes the following inferences I2 Assumptions Al A2 A3 and A4 allow the parser to infer the contents of Xo Xm and X the internal state set of the holon I3 Assumptions A5 and A6 allow the parser to infer the content of X the external state set of the holon IA Assumptions A7 and A9 allow the parser to infer X and Xj respectively the internal event set and internal controllable event set of the holon Xr the uncontrollable internal event set of the holon being given explicitly I5 Assumption A8 allows the parser to infer the content of Xp the boundary event set of the holon In relation to naming one of the consequences of these rules and assumptions is that simple state names require qualification when they are used outside of the scope of their parent OR super state
44. sing Buddy This software uses the BDD package Buddy to represent and manipulate predicates which are finite functions f D gt B Here D 0 1 p 1 is a finite domain of indexes and B 0 1 BDD packages cannot represent directly the domain of finite functions since it is multi valued as opposed to binary valued To represent finite 22 2 2 SPECIAL SUBJECTS domains they usually encode domain values using a set of BDD binary variables That means that each finite domain variable is defined by a set of BDD variables that are logically grouped together to represent the finite domain variable in question Buddy supplies a layer over the BDD basic layer that it calls finite domains or fdd in order to simplify the manipulation of finite domains predicates In order to use that facility one must include the header file ad n This header file also contains C wrapper constructs that make using many features of the BDD package easier and transparent e Many operators are overloaded in particular BDD negation is invoked through operator conjunction is invoked through operators and disjunction is invoked through operator e Dynamic memory management is taken care of automatically by the C wrap pers otherwise the user has to do it manually using routines of the BDD pack age To encode finite domains Buddy uses the encoding known as the least significant bit first encoding That means that for each finite
45. states making up the state tree of the STS model 2 a pointer to the state descriptor of the presumed root of the state tree of the STS model 3 the active state set for ST 4 the list of active state sets making up STm 5 the list of active state sets making up Data structures for STo ST and S simply use STL as they are only sets of strings or lists of sets of strings The definitions for state descriptors transition sets and 17 PROGRAMMERS MANUAL the related sets and map are contained in the module TAST cpp or rather its header TAST h This set of data structures can be seen as forming the Abstract Syntax Tree AST of the concrete syntax used for the specification of a control problem model Appendix A Despite its source code size the parser is a simple straightforward recursive descent parser with no parse error recovery That means that the parse process is terminated as soon as a single syntax error is detected In that case the parser issues the best parse error message that it can and aborts the parsing process The grammar Appendix A is very simple and parsing its syntax does not require any lookahead The next token if legal always determines the next construct and the next action that the parser should take Therefore the general parsing pattern consists in 1 looking up the current token in the input stream matching 2 if the token is not one of the expected tokens at that point then issue an error m
46. t specifications below Simple state labels must be qualified with their parent s name in order to be correctly identified since they are not registered at the global i e STS level here However structured states i e OR or AND super states must use unqualified names STO xl a bl b10 b2 b20 x2 d Set of terminal configurations of the STS given as a list of active state sets x STm baln j kkkk k kkk k k Definition of the control problem S xxx kd ok x x x KK Control specification Set of forbidden state trees given as a list of active state sets Se xl a x2 d xl a x2 e 1 2 CONTROL PROBLEM MODEL SYNTAX The Abstract Syntax Tree AST the output of the parser is formed of a set of state descriptors one of which is designated as the ST root and three special objects for STy ST and S which are given as active state sets and lists of active state sets Therefore the three main constructs of the syntax are state descriptors active state sets and transitions Transitions are part of holon descriptions All other constructs are collections of these three main constructs Note that the syntax for the main constructs is strict and assumes a specific order of appearance of their sub constructs The parser implements no parse error recovery so that a parse error stops the parse To define ST there is basically one main construct the state descriptor The header of the state d
47. table of indexes and use the STL data structure valarray lt index_t gt They represent one or more lt variable value gt pairs all on the same BDD variable Suppose vb is a variable bindings expression then vb 0 is the BDD variable number and subsequent values vb i for i 21 k represent the associated values The smallest such expression is a table containing two integers the first being the BDD variable number and the second its assigned value Such an expression represents a predicate of the form v qo More complex expressions of the form v qo q for example would use a table with more than two elements in the example a table of size 3 All predicates mentionned in item 1 and 2 above can be represented by expressions of type TPPExpr In particular by checking in 2 one can observe that the negation operator is not needed The compiler produces a few other data structures such as a variable name map to allow the BDD package to print some results Also the data structure TSFBC is provided to allow storing the result of control problem resolution 2 2 Special Subjects The following are notes on some subjects that may require clarification In par ticular Buddy is presented as a BDD package but little is said on how it can handle Finite Functions Also the subject of control function simplifications is not exhaus tively covered in 2 and requires some clarification 2 2 1 Finite Domain Predicates U
48. tion of ST takes the form of a non empty flat list of structured state definitions Structured states here are understood to be OR and AND super states The first element of that list is considered to be the root state of ST Hence in this syntax the definition of ST is not optional It must contain at least one element the root and that element must be a structured state As a consequence in this syntax neither the empty state tree nor the trivial state tree composed of a sole simple state at the root can be specified The syntax used has been designed to require a minimum of information in order to build a correct STS model and to minimize the potential of error in specification For that purpose some rules have been built into the syntax to allow the parser to infer as much as possible about the structure of the specified state trees and also about the elements of dynamic associated with OR super states the holons The first thing to notice about the concrete syntax is that the definition of ST only contains structured state definitions whereas state trees also contain so called simple states see 2 p 13 for the formal definition of simple states This has been done to remove the burden of having to assign unique names to simple states as is required in 2 Simple states in a well formed state tree can only be found as children of OR super states and their names are usually meaningful only in the context of their parent state In pa
49. variable assignment which is part of the BDD start up process Apart from variable index mapping a set of data structures must be provided to encode predicates A small class hierarchy is provided for that purpose class TPPExpr and its sub classes in source module CompilerDS cpp h The name TPPExpr stands for Type Pseudo Predicate Expression This set of classes is designed to drive the 21 PROGRAMMERS MANUAL computation of basic predicates used in control problem resolution The compiler builds these expressions for transition relations and for active state sets Part of the variable resolution process is to scan those Pseudo Predicates to replace their reference variable indexes by actual BDD variable number at BDD package start up time Once the variable of the predicates have been resolved a call to method TPPExpr eval returns a bad structure which is a BDD encoding of the expression There are three main types of expressions for TPPExpr conjunction lists disjunc tion lists and simple expressions Conjunction lists are lists of factors that must be combined with the conjunction operator of the BDD package each factor being it self a TPPExpr Similarly disjunction lists are lists of terms that must be combined with the disjunction operator of the BDD package each term being itself a TPPExpr Apart from the constants true and false simple expressions are variable bindings ex pressions Variable bindings are represented as a
Download Pdf Manuals
Related Search