Home

Helena 2.3 User's guide

1. range range expression expression mod expression 59 60 APPENDIX A SYNTAX SUMMARY Enumeration type enumeration type enum enumeration constant C enumeration constant enumeration constant x name Vector type vector type vector index type list o type name index type list x type name C type name Structured type struct type struct component y component type name component name component name x name List type ist type xm ist type name of type name with capacity expression li D gt 1 z na gt p 3 f D gt z h gt P y p Set type set type x set of type name with capacity expression Subtype subtype xe subtype name parent name constraint subtype name x type name parent name type name constraint range Constants constant xe constant type name constant name expression constant name name Functions function xe function declaration function body function prototype xe function function name C parameters specification gt type name function declaration xe function prototype function body import function prototype function prototype statement parameters specification paramete
2. property name temporal expression temporal expression x temporal expression true false state proposition name not temporal expression temporal expression temporal expression temporal expression and temporal expression 11 temporal expression temporal expression temporal expression until temporal expression 30 CHAPTER 1 HELENA SPECIFICATION LANGUAGE Using Helena 2 1 Invoking Helena Using Helena consists of writing the description of the high level net in a file called the net file thereafter e g my net lna and the properties expressed on this net in a second file called the property file thereafter e g my net prop lna and to invoke Helena on this file The command line of Helena has the following form helena option option my net lna When invoked Helena proceeds as follows 1 If the net described in file my net 1na is my net the directory helena models 1na my net is created 2 A set of C source files and a Makefile are put in directory helena models lna my net src 3 These files are compiled and an executable is created which corresponds to the actual model checker for the specific net 4 The compiled executable is launched 5 Once the search is finished a report is displayed on the standard output If a property was checked this report indicates whether the d
3. state propositions x load not balanced for each couple of servers s1 s2 with sl 52 the difference between the number of requests pending or accepted by x sl and the number of requests pending or accepted by s2 is at most l proposition load_not_balanced not forall sl in server_id s2 in server_id sl s2 diff card sr in server_request sr gt 2 sl card sn in server notification sn 1 81 card sr in server request sr gt 2 s2 card sn in server notification sn gt l s2 lt 1 proposition balancing balancer balancing card 1 Listing 3 4 Helena file of the load balancing system properties file examples load balancer prop lna 1 any deadlock state state property not dead reject deadlock the loads are balanced or are being rebalanced state property balance ok reject load not balanced accept balancing 00 ON t R Q D BRR A UU WWW WWW Q2 D ND ND ND D D D t R2 FB BR BRR RR Re WN 0 A On HB D O 0 A LU HB D EO MO 0 Ia Li D COO 3 3 THE TOWERS OF HANOI 45 3 3 The towers of Hanoi The towers of Hanoi is a well known mathematical game It consists of three towers and a number of disks of different sizes which can slide onto any tower The puzzle starts with the disks neatly stacked in order of size on one tower smallest at the top thus making a conical shape The objective
4. A set of cyclic processes Incrementation of the local variable Clients Servers AR AO c s 7 c Requests 0 o a 5 Acks sc 55 Q gt CN may A om ro RO An incrementation of the shared variable 7 A lock guarantees exclusive access to 7 A synchronous exchange between clients and servers Process place amp Protected place OBuffer place 4 3 Local place Shared place Oax place Graphical representation of the different place types Figure 5 1 Four example nets illustrating the possibility of place typing 5 3 2 Safe transitions Objects Q Working o P Figure 5 2 Transition Release is safe Take is not 5 3 GUIDING HELENA IN THE SEARCH 57 Transitions of the net can be declared as safe A transition binding is safe if it cannot be disabled by the firing of another binding In other words the tokens consumed by the binding cannot be stolen by another binding If a transition of the net is declared as safe then Helena considers that all the possible bindings of the transition are safe Figure 5 2 depicts an example of safe transition Each process can be in place dle in place Working To go to work a process must first acquire an object o The objects are initially in the place Objects When a process returns to place Idle it puts back the object in place Objects A token p o in place Taken means that process p has taken object
5. Help 5 1 Evaluation of Transitions 5 1 1 Evaluation in the absence of inhibitor arcs 5 1 2 Evaluation in the presence of inhibitor arcs 32 Lips and TICKS so a s Book a 5 3 Guiding Helena in the search sss ss ss nen six Sal BAS Ba oa R 5 3 2 Safe anson AA Syntax summary A 1 Net specification language A2 Property specification language oo occiso en ee n Gnu general public license CONTENTS Helena specification language We introduce in this chapter the two specification languages of Helena used to describe high level nets and properties 1 1 Lexical and syntaxic conventions We give now some lexical conventions First of all it must be noticed that Helena specification language is case sensitive 1 1 1 Lexical tokens 1 1 1 1 Reserved words The following words are reserved and can not be used as identifiers accept and assert capacity card case constant deadlock default description dom else empty enum epsilon exists false for forall function guard if import in init inhibit let list 1tl max min mod mult not of or out pick place pred priority product property proposition range reject return safe set state struct subtype succ sum transition true type until vector while with Reserved words will systematically appear in a bold font in this document 1 1 1 2 Identifiers Places data types and transitions are examples of He
6. transition state proposition 1 2 2 Net parameters A net may have parameters such as e g a number of processes They are interpreted as constants see Sect 1 2 4 of the predefined int type The advantage of using parameters is that their values can be changed via the command line when helena is invoked i e without changing the model file Chapter 2 details how this can be done Below is an example of net parameterized by constants Clients et Servers having default values of 5 and 2 respectively myNet Clients 5 Servers 2 1 2 NET SPECIFICATION LANGUAGE 9 net parameter net parameter net parameter list net parameter name number name net parameter list net parameter net parameter name x 1 2 3 Types and subtypes Helena allows the definition of different kinds of data types integer types range or modulo types enumeration types structured types vector types and container types list or set types Enumeration and integer types form the family of discrete types whereas other types are said to be composite This type hierarchy is summarized below e Discrete types Integer types Range types Modulo types Enumeration types e Composite types Structured types Vector types Container types Settypes Listtypes Some data types are predefined They will be described in the corresponding type description type
7. Ls state propositions proposition site waiting waiting card gt 0 r T T T gt gt gt gt 39 Listing 3 2 Helena file of the distributed database system properties file examples dbm prop lna Un amp D rR 40 CHAPTER 3 EXAMPLES a site waiting for answer will eventually leave this state ltl property bounded wait site_waiting gt lt gt not site waiting 3 2 The load balancing system We propose to specify and verify a simple load balancing system with Helena The full net is illustrated by Figure 3 2 Initial markings and transition guards have been omitted to clarify the figure CLIENTS LOAD BALANCER SERVERS c least 1 gt bal idl S st 5 idl T alancer idle decrncr least 1 most l J server_idle client_idle 1 lt 1 gt s Ge s c 1m 1 9 0 teder LE s A erver notification Y client send Y y balancer_feceive_client x balancer recdive notificitio E server notify A 1 8 i a Yat c c client request Le al 2 de A 5 1 GO sc Al y Ca H ates g 1 5 iv v server nolification ack server waiting client waiting balancer_routin balancer_balancin Tooske y s l A s El lt 1 gt lt 1 gt e c 1 c 2 3 lt s c gt lt s gt V S Y A Y To 1 client rec
8. expression expression expression expression expression expression expression expression expression 75 expression 4 expression expression Comparison operators comparison operation expression expression expression 1x expression expression 75 expression expression gt expression expression expression expression expression Boolean logic boolean operation expression or expression expression and expression not expression Variables variable variable name structure component vector component list component pou A 63 numerical constant variable integer operation boolean operation cast structure structure assignment vector component empty list list component list slice list membership set set operation attribute Structures structure structure component structure assignment Vectors vector vector component vector assignment Lists empty list list list component list assignment list slice list concatenation list membership Sets empty set set set membership xx set operation Function call function call Cast cast nm If then else if then else condition true expression xm false expression xx Token componen
9. it contains the list sie H proposition all_moved exists t in towers t 1 tower last and t gt 2 full Listing 3 6 Helena file of the towers of Hanoi properties file examples hanoi prop lna we reach a state in which all disks have been moved to the last tower state property end_state reject all_moved QO IN Un WN Interfacing Helena with C code Although the language provided by Helena for arc expressions is quite rich it may not be sufficient and the user may for instance prefer to use its own C functions rather than writing these in the Helena specification This is provided by the language through the import construct As the code generated by Helena is written in C all imported components have to be written in this language This chapter first starts with a tutorial illustrating the use of this feature 4 1 Tutorial Importing C Functions Our goal is to simulate the quick sort algorithm with Helena The net we want to analyze consists of a single transition swap that takes a list of integers from a place myList swaps two of its elements and put its back in place myList Each occurence of this transition simulates a single step of the quick sort algorithm The list we want to sort toSort is a constant initialized via function initList Below is the definition of this net Listing 4 1 Helena file of the sort net file example sort 1na Maa ook eee eee ee ee eee ee ee ke SR GR k k
10. k k k a ee load balancer C 7 x number of clients x S 2 number of servers x Je clients x type client id range 1 C type clients no range O client id last servers type server id range 1 S load type servers load vector server id of clients no constant servers load empty load 0 return the least loaded server x function least servers load load server id server id result server id first for i in server id if load i load result result i return result return the most loaded server x function most servers_load load gt server_id server_id result server_id first for i in server_id if load i gt load result result i return result check if load is balanced function is balanced servers load load bool clients no max no 0 clients no min no clients no last for i in server id if load i gt max_no max_no load i if load i min no min no load i return max no min no lt 1 increment the load of server i x function incr servers load l server id i servers load 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 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
11. true expression expression false expression x expression 1 2 9 10 Structures Structures can be handled in Helena in three different manners Firstly a structure can be constructed by placing all its elements between characters and In this case the expression is of any structured type which have the same number of components as the structure In addition each expression of the structure has to be of the same type as the component declared at the same position in the structured type For instance if we consider the following type declaration type t struct int i bool b the expression 35 false has at least type t Its first component i has value 35 and its second component b has value false A second possibility to manipulate structures is to access a component of the structure If we let s be an expression of type t s i denotes the value of the component i of s This expression is only valid if t is a structured type which has a component 1 2 NET SPECIFICATION LANGUAGE 21 named i If these conditions are met the type of s i is the type of component i in the declaration of t and its value is the value of the component i of s Please note that we do not allow constructions such as 10 false i The structure accessed must be a variable At last structures can be manipulated by using the operator This construction is a shortcut to assign an expression to a component of a structure Let
12. For an enumeration constant the resulting expression is of any enumeration type which includes the constant number name numerical constant c enumeration constant 1 2 9 2 Variable We call variable any expression which can be assigned a value It is either a simple variable either a component of a structure a vector or a list The type of the expression depends on the declaration of the variable Structure vector and list components will be described later in the section variable name structure component vector component list component variable 0 1 2 9 3 Predecessor and successor operators The succ and pred operators allovvs to pick the successor and predecessor of a discrete value Let t be a discrete type and e be an expression of this type e If t isa numerical type pred e is equivalent to e 1 and succ e is equivalent toe 1 An error may be raised if t isa range type and the pred resp succ operator is applied on the first last value of the type e If t is an enumeration type the evaluation directly depends on the declaration of the t For instance if we consider the following declaration 1 2 NET SPECIFICATION LANGUAGE 19 type color enum red green blue then we have succ red green pred blue and succ blue red predecessor successor operation pred expression suee expression 1 2 9 4 Integer arithmetic All the classical operators are allow
13. amp arr l amp arr beg nb quickSort arr beg 1 nb quickSort arr r end nb TYPE_intList IMPORTED FUNCTION quickSort TYPE intList 1 TYPE int nb TYPE intList result 1 quickSort result items 0 result length amp nb return result Je File isSort d c 7 include sort interface h TYPE bool IMPORTED FUNCTION isSorted TYPE intList 1 int i 0 for i 0 i l length 1 i if l items i gt 1 itemsli 11 return TYPE ENUM CONST bool false return TYPE ENUM CONST bool true Figure 4 1 Imported functions of the tutorial 4 2 THE INTERFACE FILE Table 4 1 Mapping Helena types to C Helena type C type Numeric types type small range 0 255 typedef short TYPE_small type big range 0 65535 typedef int TYPE_big Enumerate types type color enum typedef char TYPE_color red define TYPE__ENUM_CONST_color__red 0 green define TYPE__ENUM_CONST_color__green 1 blue define TYPE ENUM CONST color blue 2 yellow define TYPE__ENUM_CONST_color__yellow 3 cyan define TYPE__ENUM_CONST_color__cyan 4 Vector types type colors vector color bool of int typedef struct TYPE int vector 5 2 TYPE colors Structured types type rgbColor small r small g small b struct b typedef struct TYPE_small r TYPE_small g TYPE_small b TYPE_rgbColor Container types type colorLis
14. capacity 1 type ack site id ifdef UNUSED place unused dom site id init for s in capacity 1 type buffer site id site id endif site id s modelling communication r in N number of sites x control flow of processes gt channels site id if s r s r 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 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 3 1 THE DISTRIBUTED DATABASE SYSTEM place mutex dom epsilon E init epsilon capacity 1 type shared transition update and send s gt epsilon for r in site id if s r s s for r in site id if s r s s for r in site id if s r s s gt epsilon for r in site id if s r lt s transition receive message lt r lt s r r s r r s r lt r lt s r in inactive mutex ifdef UNUSED unused endif out waiting sent transition receive_acks in waiting acks out inactive mutex ifdef UNUSED unused endif in inactive sent out performing received transition send_ack in performing received out inactive acks
15. in type name range variable name in place name variable name in expression pc 1 2 8 8 Assertion Assertions can also be placed in functions As for transitions the boolean expression associated to an assertion is checked and if this expression is evaluated to false the search is immediately stopped assert statement assert 1 2 9 Expressions Helena has been primarily designed to manage the verification of realistic software systems Thus we naturally decided to include in Helena a wide range of possibilities concerning expressions Some remarks e Each expression has a single type that Helena tries to guess at the parsing stage When Helena has to choose between several types for a given expression the widest possible type is chosen For instance 0 gt 2 will be considered as a comparison between two constants of type int If Helena can not choose between different types an ambiguity error will be raised e Iterators and token components are special kinds of expressions that can only appear in a property specification These form the family of complex expressions Attributes related to a place also belong to this family e An expression is said to be statically evaluable if no variable and no function call appear in all its sub expressions 18 CHAPTER 1 HELENA SPECIFICATION LANGUAGE e Expressions may raise errors at the run time such as division by 0 cast error Out of range errors form a spec
16. in p x f y gt out q x pick y in g x g returns a set of integers For transition t the tuple lt x f y gt defines variable x but to evaluate it we require that y must be defined The tuple lt y x 2 gt defines this variable but needs itself variable x to be defined Hence there is here a cyclic dependency We face the same problem for transition u The invokation of Helena on this example will raise the following errors 53 54 CHAPTER 5 HELP test lna 4 Transition t cannot be evaluated test lna 8 Transition u cannot be evaluated 5 1 2 Evaluation in the presence of inhibitor arcs Tf the transition has inhibitor arcs then the process described in the previous section first takes place If we have found some binding for the variables defined in the input tuples or in the pick section of the transition then a second evaluation process starts for the inhibitor arcs of the transition To be firable there must not be any binding for the variables defined by inhibitor arcs such that the corresponding tokens are present in the place linked by the inhibitor arc Let us for instance consider the following transitions transition t in p x out q lt x gt inhibit r lt x gt transition u in p lt x gt out q lt x gt inhibit s lt x y gt Transition t is firable for some binding x if and only if the token lt x gt is present in p but
17. of these variables In Helena these variables are not explicitely given in the definition of the transition A variable is implicitly declared if it appears in an arc between the transition and one of its input places at the top level 1 e not in a sub expression and in a non guarded tuple see Section 1 2 10 2 for more details on tuples The user may also let Helena bind a variable by picking its value in a specific domain We call these variables the free variables of the transition and they appear in the pick section of the transition Rather than repeating the same expression it is also possible to assign this expression to a bound variable declared in the let section and then replace the expression by the bound variable wherever it occurs The reader may find in Section 5 1 a brief description of the algorithm used by Helena to evaluate transitions and the conditions under which a transition is evaluable Transitions in Helena are identified by a name The description of a transition must specify the input and output places of the transition followed by inhibitor arcs if any free variables if any bound variables if any and finally its attributes a guard a priority a description and a safe attribute transition xe transition transition name 4 transition inputs transition outputs transition inhibitors transition free variables transition bound variables transition attribute y name in
18. t 22 5 The cumulated multiplicities of the tokens in p which have their second component equal to true is 5 These tokens are lt 1 true gt lt 2 true gt and lt 4 true gt 1 2 NET SPECIFICATION LANGUAGE 27 min t in p t gt 1 1 max t in p t gt 1 8 The minimal and maximal values for the first component of all the tokens in place p are 1 for token lt 1 true gt and 8 for token lt 8 false gt sum t in p t gt 2 1 7 The sum of the first components of the tokens which have their second component equal to true is 7 1 2 4 product t in p not t 22 t gt 1 16 The product of the first components of the tokens which have their second component equal to false is 16 8 2 exists i in t forall b in bool card t in p t gt l i and t gt 2 b 1 This expression can be read as fol lows there is an element i of type t which is such that the tokens lt i false and i true are present in place p This holds for i22 iterator ze iterator type iteration scheme iterator condition iterator expression iterator type forall exists card mult min max sum product iterator condition x expression iterator expression x expression 1 2 10 Arc labels In high level Petri nets arcs between places and transitions are labeled by expressions indicating for a given instantiation of the v
19. 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 3 2 THE LOAD BALANCING SYSTEM dom server_id capacity 1 place server_notification_ack dom server_id capacity 1 place server_request dom client_id server_id capacity 1 transition server_notify in server idle lt s gt server_request gt lt c S gt out server_waiting 2 s Ss Ie server notification s gt description server 58 16 process notification s transition server_receive in server_waiting lt S c server notification ack s gt out server processing 1 lt s c gt description server d reception of request from client 58 transition server_send in server processing s c gt out server_idle 1 lt s gt client_ack co gt description server 6d send response to client _ d 8 c y load balancer process El place balancer_idle dom servers_load init lt empty_load gt capacity 1 place balancer_routing dom servers load x client id capacity 1 place balancer_balancing dom servers_load capacity 1 transition balancer_receive_client in balancer_idle lt 1 gt client_request lt c gt out balancer routing lt 1 c description lb recei
20. 47 lare Y y out larc yop inhibit arc Y transition guard transition priority transition description safe transition name transition inputs transition outputs transition inhibitors transition attribute 1 2 6 1 Arcs An arc is characterized by the place from which we remove add or check tokens and by an expression specifying for a given instantiation of the variable of the transition considered tokens The description of arc labels appear later in this section arc x place name arc label 1 2 6 2 Free variables Free variables must appear in the pick section of the transition The value of a free variable can be picked within e adiscrete type A range can be specified to avoid considering all possible values of the type e Or a container i e a set a list Note that variables of the transitions may appear in the definition of free variables When computing enabled bindings at some marking Helena considers all possible values that can be picked for free variables For example the following pick section pick i in int range 1 5 b in bool 14 CHAPTER 1 HELENA SPECIFICATION LANGUAGE will potentially multiply by 10 the number of enabled bindings of the corresponding transition since we will generate all the possible values of i b 1 2 3 4 5 x false true transition free variables x pick free variable y f
21. aN a ee 2 1 24 Search opHOHS 2264 bane sages ie ean pe eek Pawn sem Fada buse 213 Reduction techniques 2 2 s opo cox ae SA Ra A Re ri de eS 21454 Search UB LL Les um ba ae BS e Bie aD qe eie er en ewe Bee i EES 2 1 5 Model opuons es 5 24 cmo omo A ewe s r r Bron 2 100 Output cian a tee awe RU et Pea Soe Wiee ee de e de x eese Dee aus o e x eke eee 4 Bom eee ek Pe ewe nt ek baw fas 221 Siructure OF ilie report soe oso ms RE pm RR CRGA we op GR che So a ba Ge hE aS Bes BREA E ESPOSA A e ueque de esp BO verb ee der ded 2 3 lt Additionalatlities 054405446 wee x oo oko EER ewe SE Re 23 DhehelenadopoPCHHIEy uuu chee ae ER Raya eR SOY ROS OR OY RAS eue 202 Whelhelena orapnuility s s nea a a da ADS AS RES Barge 2 3 3 helena generate interface utility 3 Examples 34 The distributed database System o o terne ERAS DR Aa RU D a E 3 2 Th load balaneme System ou ade m erem te de ds dre Be e be wh md 3 4 Th towers on HANOL se 2c eRe ER A nt du Nob 3 oo 00 O0 O0 A A A b t T t ND BRR RR 00 00 00 A N Un Un RK Interfacing Helena with C code 4 1 Tutorial Importing C Functions 42 The mterace file 2222 aa oa 42 1 Generated types canan see ER es 4 22 Generated constants and functions 4 3 Requirements on imported modules
22. faster e If no error is found during the first stage use the default storage method without compression technique e If the second search ran out of memory use compression techniques option delta and rerun the search Run time checks Enabling run time checks usually slows the analysis since additional code is put in the generated code to check that no error occurs When the net contains many arithmetic operations the run time can grow significantly Thus we advise to disable run time checks if no error is suspected in the model Expressing properties Analysis techniques and reductions i e partial order reduction performed by Helena depends on the property to be checked The reduction observed decreases with the complexity of the property Thus try to verify properties separately when possible For instance instead of verifying p and q verify first p and then q 5 3 GUIDING HELENA IN THE SEARCH 55 Depth vs Breadth first search Depth option algo DFS and breadth first search option algo BFS both perform a full state space search Depth first search usually leads to better reduction than breadth first search especially when par tial order methods are used option partial order Breadth first search however reports counter examples of minimal length Thus keep in mind these two factors when choosing the type of search to apply Though the techniques implemented in Helena are fully automatic and do not require any assista
23. for numeric types e Each value val of an enumerate type t is mapped to a macro TYPE ENUM CONST t val that is expanded to the position minus 1 of the value in the list that defines the enumerate type Note that some names are actually quite long The reason is that we thus avoid name conflicts in the generated code e A vector type vt is mapped to a structured type containing a single array element called vector The dimension s of this array match es with the cardinal s of the type s used to the define the Helena vector type In our ex ample the integer at index blue false of a C variable var of type TYPE_colors can be accessed as follows var vector TYPE__ENUM_CONST_color_ blue TYPE__ENUM_CONST_bool__ false 50 CHAPTER 4 INTERFACING HELENA WITH C CODE E File imitlist e 7 include sort_interface h TYPE_intList IMPORTED_FUNCTION_initList TYPE_intList result result length 5 result items 0 result items 1 result items 2 result items 3 result items 4 return result Il Il DOS A File quickSort c x include sort_interface h void swap int xa int xb int t xa xa xb sb t void quickSort int arr int beg int end int nb if end gt beg 1 int piv arr beg 1 beg 1 r end while 1 lt r if arr 1 lt piv 1 else if nb return swap amp arr 1 amp arr r nb if xnb 0 return swap
24. level nets of Helena domains of places are products of basic data types Tokens are denoted by lists of expressions placed between the two symbols lt and gt The same token may appear several times in a place We call multiplicity of a token the number of repetitions of this token in the place The marking of a place will be noted as the linear combination of the tokens in the place For instance the marking 2x lt 1 false gt 4x lt 2 true gt of the place p defined as place p dom int x bool is the marking which contains 2 occurrences of token lt 1 false gt and 4 occurrences of token lt 2 true gt In others words the multiplicity of token lt 1 false gt is 2 the multiplicity of token lt 2 true gt is 4 and the multiplicity of all the others tokens is 0 The domain is the only attribute that must be specified by the user Several optional attributes of the place can also be defined place place place name place domain place attribute place attribute x initial marking capacity place type 12 CHAPTER 1 HELENA SPECIFICATION LANGUAGE 1 2 5 1 Domain Domains of places are products of basic data types The keyword epsilon is used to denote the empty product In this case the place is equivalent to an ordinary Petri net place Each time a place is declared a type is implicitly declared which correspond to the domain of the place This type belongs to a special family
25. name variable name expression name variable declaration x variable declaration variable name n Places place place attribute place place name place domain place attribute y initial marking capacity place type Domain domain ze dom domain definition domain definition epsilon types product types product type name x type name Initial marking initial marking lt init marking marking 1 arc label Capacity y 15 capacity capacity expression 62 APPENDIX A SYNTAX SUMMARY Type place type type place type name place type name process local shared protected buffer ack Transitions transition transition transition name 17 transition inputs transition outputs transition inhibitors transition free variables transition bound variables transition attribute 3 transition name name transition inputs in f arc y transition outputs out O lar y transition inhibitors inhibit 47 arc transition attribute transition guard transition priority transition description safe Arcs arc place name Free variables transition free variables free variable free variable domain Bound varia
26. of a storage or distribution medium does not bring the other work under the scope of this License You may copy and distribute the Program or a work based on it under Section 2 in object code or executable form under the terms of Sections 1 and 2 above provided that you also do one of the following a Accompany it with the complete corresponding machine readable source code which must be distributed under the terms of Sections 1 and 2 above on a medium customarily used for software interchange or b Accompany it with a written offer valid for at least three years to give any third party for a charge no more than your cost of physically performing source distribution a complete machine readable copy of the corresponding source code to be distributed under the terms of Sections 1 and 2 above on a medium customarily used for software interchange or c Accompany it with the information you received as to the offer to distribute corresponding source code This alternative is allowed only for noncommercial distribution and only if you received the program in object code or executable form with such an offer in accord with Subsection b above 69 The source code for a work means the preferred form of the work for making modifications to it For an executable work complete source code means all the source code for all modules it contains plus any associated interface definition files plus the scripts used to control compilation a
27. of statistics displayed depend on the option passed to Helena For instance no statistic concerning the reachability graph are available in a fast simulation mode 2 2 2 Generating reports Helena can produce an XML report file corresponding of the report displayed when it is invoked with option report file The purpose of XML reports is to ease the interface between Helena and other tools 2 3 Additional utilities Together with Helena are installed several utilities that we briefly describe here 2 3 1 The helena report utility The purpose of helena report is to print an XML report that has been created by Helena This utility is useful in the case where you have already invoked Helena on a net and you do not want to launch the search again Here is an example of use of this utility helena my net lna helena report my net where my net is the name of the net of file my net 1na The search report will then be printed to the standard output Alternatively you can directly pass to helena report an xml report previously generated For example the following sequence of commands is equivalent to the previous one helena report file my_report xml my net lna helena report my_report xml 2 3 ADDITIONAL UTILITIES 35 2 3 2 The helena graph utility Helena can build the reachability graph of net in order to display some statistics on e g its strongly connected components This is the purpose of the action BUILD GRAPH option This o
28. of the game is to move the entire stack to another tower obeying the following rules e Only one disk may be moved at a time e Each move consists of taking the upper disk from one of the towers and sliding it onto another tower on top of the other disks that may already be present on that tower e No disk may be placed on top of a smaller disk This example illustrates the use of lists in Helena Listing 3 5 Helena file of the towers of Hanoi file examples hanoi 1na Pate k kk k k k k k k k k k k k k k CCCI ee ee dd k R k k k k k k k ICCA k k k k k k x Example file of Helena distribution x File hanoi lna x Author Sami Evangelista s Date 2 13 feb 2007 This file contains the description of the towers of Hanoi game He ee He D k k k k sk k k 00 hanoi N 3 Je oN the number of disks x M 3 x M number of towers identifier of a disk type disk range 1 N identifier of a tower type tower range 1 M a list of disks type disk list list nat of disk with capacity N construct the list of disks initially present on the first tower function construct towerl gt disk list disk list result empty for i in disk result i amp result return result this unique place models the state of the towers in the initial marking the first tower contains the list IN fl and al
29. shared place since processes compete for the acquisition of this lock Buffer and ack places Figure 5 1 bottom right Processes can also synchronize themselves by sending messages on communication channels These channels are modeled by buffer places These places can be thought of as shared places but there is a major difference between the two a token residing in a buffer place can only be removed by a single process Thus channels represented by buffer places are multiple senders single receiver channels Ack places are special kinds of buffer places used to represent acknowledgments of synchronous exchanges For instance if process p sends a message to process p then waits for the acknowledgment of p before continuing its execution the place which corresponds to the acknowledgment can be typed as ack The depicted net models the behavior of a set of clients which interact through messages exchanges A client c sends a request to a server s by putting a token c 5 in place Requests Since the only server which can receive this request and withdraw the token c s from place Requests is s we can type this place as a buffer place Once received by the server the request is treated and an acknowledgment is sent to the client which can continue its execution Since this exchange is a synchronous one the place Acks can be typed as an ack place 56 CHAPTER 5 HELP Idle p Working EA p LP
30. xe function prototype function body xe import function prototype function prototype 000 parameter specification C parameter specification parameters specification xe type name parameter name parameter specification function name parameter name name name 1 2 8 Statements Helena allows rich possibilities to write functions conditional statements if case loop statements for while sequence of statements block assertions and naturally the return and assignments statement Except for the for statement each has the same semantic as C s corresponding statement assignment if statement case statement while statement for statement return statement assert statement block statement xx 16 CHAPTER 1 HELENA SPECIFICATION LANGUAGE 1 2 8 1 Assignment The assignment statement evaluates an expression and assigns its value to a variable The variable assigned can be a simple variable a structure component a vector component or a list component Assigned expression must naturally have the same type as the variable assignment variable expression 1 2 8 2 If then else An if statement evaluates a boolean expression and according to its value executes either the true statement either the false statement if it exists if statement 18 expression true statement else f
31. y container attribute APPENDIX A SYNTAX SUMMARY 22 component name expression false expression card capacity prefix suffix A 2 PROPERTY SPECIFICATION LANGUAGE 65 Iterator iterator xe iterator type iteration scheme iterator condition iterator expression 1 iterator type forall exists card mult min max sum product iterator condition expression iterator expression x expression Arc labels arc label complex tuple C complex tuple Tuples complex tuple x tuple for tuple guard tuple factor tuple tuple for for iteration scheme tuple guard if expression tuple factor xe expression x tuple xe lt non empty expression list gt epsilon State propositions state proposition xe proposition state proposition name expression state proposition name x name A 2 Property specification language Properties property specification property property state property temporal property State properties state property state property property name state property definition property name name state property definition reject clause accept clause reject clause xe reject predicate accept clause a
32. 42 return 1 lil 1 i 1 x decrement the load of server i x function decr servers_load 1 server_id i gt servers_load return lil l i 1 return the difference between the two loads x function diff clients no cl clients no c2 clients return cl gt c2 cl c2 c2 cl f clients place client idle dom client_id init for c in client id c gt capacity 1 place client_waiting dom client_id capacity 1 place client_request dom client_id capacity 1 place client_ack dom client_id capacity 1 transition client_send in client_idle 0c out client waiting c client request c gt description client d send request c transition client_receive in client waiting c gt client_ack lt c 5 out client idle lt c gt description client d _ receives response c servers place server idle dom server id init for s in server id s gt capacity 1 place server_waiting dom server_id client_id capacity 1 place server_processing dom server id x client id capacity 1 place server_notification CHAPTER 3 EXAMPLES 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
33. CIFICATION LANGUAGE Type attributes Let t be a discrete type of the net t first and t last correspond to the first and the last value of t Their value depends on the definition of t e Ift is arange type defined as range low up then t first low and t last up e If t is a mod type defined as mod N then t first 0 and t last N 1 e If t is an enumeration type t first it is the first element in the list which defines t and t last it is the last element of the list t card is the cardinal of type t This expression can have any numerical type Its value depends on the definition of t e Ift is a range type defined as range low up then t card 1 up low e Ift isa mod type defined as mod N it is N e If t is an enumeration type it is the length of the list which defines t Some examples e bool first false e bool last true e bool card 2 Place attributes Let p be a place of the net p card is the number of tokens in place p at the current state This expression can have any numerical type p mult is the cumulated multiplicities of the tokens in place p at the current state This expression can have any numerical type For instance if place p contains the following tokens at the current state 2 lt 2 true gt lt 3 false gt 4x lt 5 false gt Then we have p card 3 and p mult 7 Indeed there are three different tokens in place p at the current state and the sum of the mul
34. For example to express that no deadlock can occur we can write state property not dead reject deadlock Now to specify that the termination state is a valid deadlock state we can write state property not dead2 reject deadlock accept valid termination where state proposition valid termination has been defined in the net specification as proposition valid termination termination card gt 0 state property state property property name state property definition property name name state property definition reject clause accept clause reject clause n reject predicate accept clause me accept predicate predicate uz deadlock state proposition name 1 3 PROPERTY SPECIFICATION LANGUAGE 29 1 3 2 Temporal properties Helena can also analyse LTL properties An LTL property is defined by a name and a temporal expression To be verified all maximal executable sequences must match the expression specified A temporal expression is built using state propositions Besides usual boolean operators a temporal expression can also include the following temporal operators globally lt gt finally and until For instance the following temporal property expresses that once state proposition p holds it holds in all subsequent states of the sequence It property prop not P or P temporal property 161
35. Helena 2 3 User s guide Sami Evangelista Sami dot Evangelista at lipn univ paris13 dot fr March 28 2013 Abstract This manual describes Helena a High LEvel Nets Analyzer Helena verifies properties of high level nets by exploring all these possible configurations and reports to the user either a success i e the property holds either a faulty execution invalidating the specified property This technique is called model checking or state space analysis Helena can also perform more basic tasks like state space exploration in order to report statistics like e g the number of reachable statistics the structure of the reachability graph Helena is a command line oriented tool freely available under the terms of the GNU General Public License Basic knowledges on Petri nets high level Petri nets and model checking are welcome to understand this manual The installation on a Linux platform is quite simple and should not raise any problem The procedure is detailed in file helena README This manual is organized as follows The specification language of Helena is presented in Chapter 1 Chapter 2 is devoted to the use of Helena Some examples of the distribution are described in Chap ter 3 The possibility of interfacing Helena with C code is described in Chapter 4 together with a tutorial illustrating this feature At last Chapter 5 is intended to provide some help to the users and some indications on how to use Helena efficientl
36. LAR PURPOSE THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU SHOULD THE PROGRAM PROVE DEFECTIVE YOU ASSUME THE COST OF ALL NECESSARY SERVICING REPAIR OR CORRECTION IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING WILL ANY COPYRIGHT HOLDER OR ANY OTHER PARTY WHO MAY MODIFY AND OR REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE BE LIABLE TO YOU FOR DAMAGES INCLUDING ANY GENERAL SPECIAL INCIDENTAL OR CONSEQUENTIAL DAM AGES ARISING OUT OF THE USE OR INABILITY TO USE THE PROGRAM INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES END OF TERMS AND CONDITIONS Index arc label 27 arc expression 27 tuple 27 constant 11 expression 17 attribute 23 container attribute 24 list attribute 22 25 list membership 22 place attribute 24 type attribute 23 boolean operation 19 cast 20 comparison operation 19 constant 18 function call 20 if then else 20 integer operation 19 iterator 26 list operation 21 empty list 21 list assignment 22 list component 22 list concatenation 22 list constructor 22 list slice 22 predecessor successor operation 18 set operation 23 empty set 23 set constructor 23 set membership 23 set union intersection differen
37. after it is defined If it is defined and the ifdef has a corresponding else all the lexical tokens between the corresponding else and endif are ignored Otherwise all the lexical tokens are skipped until the corresponding else or endif is found Directive ifndef has a symmetric behavior 1 13 Conventions We first start with some conventions that are used in the remainder of this section e Terminal symbols of the grammar i e tokens are placed between quotes e g if transition e Non terminal symbols appear in italic between the two characters and e g expression statement e denotes the empty list of lexical tokens e The non terminal name stands for any identifier e The non terminal string stands for any string delimited by two characters e The non terminal number stands for any numeric constant e Symbols placed between brackets are optional e g item e item is a sequence possibly empty of non terminals item item is a non empty sequence of non terminals item 1 2 Net specification language 1 2 1 Nets A net is described by a list of definitions that are the components of the net Elements that may be defined in a net are data types constants functions places transitions and state propositions net parameter list gt U definition y net name x name definition x type net net name iv constant function place
38. alse statement true statement statement false statement statement 1 2 8 3 Case A case statement evaluates an expression and according to the value of this expression chooses an appropriate alternative A default alternative can be defined Expressions which appear in the alternatives must have the same type as the evaluated expression and must be statically evaluable In addition two different alternatives can not have the same expression All possibilities may not be covered If an alternative is not covered and the evaluated expression falls into this alternative the case statement has no effect case expression case alternative default alternative 3 expression statement default statement case statement case alternative default alternative 1 2 8 0 Return A function returns a value by a return statement An expression is evaluated which correspond to the value returned by the function The type of this expression must be the return type of the function in which the return statement appear All state ments appearing after the return statement are ignored return statement return expression 1 2 8 5 Block A block is a list of variables or constants declarations followed by a sequence of statements A block start with the token and terminates with the token Each variable declared in the block is naturally visible as soon it is declare
39. ariable steps of transition swap is used to count the number of swaps we have to perform with quick sort algorithm Note that the function quickSort is always called with list toSort Hence place myList will successively contain the following token toSort quickSort toSort 1 quickSort toSort 2 quickSort toSort 3 until the function returns a sorted list Now let us suppose that we do not want the functions used in this net to be written in Helena but directly in C The easiest solution is to use the import feature of Helena Note that after these imports the bodies of these functions do not have to be declared This would actually be an error Lastly in order to follow the sequence of swaps performed by quick sort we write the following line in the property file state property not_dead reject deadlock In order to write these C functions we need to know how the types of their parameters have been mapped to C This is the purpose of the helena generate interface tool that is invoked with only two parameters as below helena generate interface sort lna sort_interface h File sort interface h is the resulting C header file that contains all declarations that could be required by the user to write his her imported functions We only provide here the declarations that are required for the understanding of this tutorial Looking at the net specifica tion we need to access the declarations of types int intList and bool These three t
40. ariables of the transition the tokens consumed or produced by the firing In the high level nets supported by Helena these expressions are linear combinations of simpler ones called tuples of expressions or more simply tuples Tuples are lists of expressions placed between two tokens lt and gt For instance given two variables x y the expression 2 x y lt y 0 gt produces two tokens of type lt 0 1 gt and one token of type lt 1 0 gt for the instantiation x 0 y 1 1 2 10 1 Arc expression As stated previously an expression labeling an arc of the net is a linear combination of tuples or a sum of complex tuples Both are defined just afterwards arc label complex tuple 4 complex tuple 1 2 10 2 Tuples Tuples are basic components of arc label They may be guarded by a boolean expression If this expression is evaluated to true for the firing instantiation the corresponding tokens are normally produced Otherwise if the condition does not hold tokens are not produced A condition can be specified by placing a construction if cond before the tuple For instance let us consider the tuple if x 0 x If x lt the tuple does not produce any token else it produces a single token x Helena also provides the following syntactical facility instead of writing lt x false 1 gt lt x false 2 gt lt x true l gt lt x true 2 gt one can prefix the tuple with some iter
41. ation scheme see Section 1 2 8 7 for b in bool i in int range 1 2 lt x b i gt Note that we do not allow the iteration variable to loop over places or containers Only discrete iteration variables are allowed In addition if a range is specified for an iteration variable then it must necessarily be evaluable statically 1 e the two bounds must be evaluable statically The two possibilities can also be combined For instance for b in bool i in int range 1 2 if x 1 or b lt x b i gt is a valid tuple If the domain of the corresponding place is the empty product epsilon the only possible tuple is epsilon The expressions list in the tuple must correspond to the domain of the corresponding place A factor may appear before the tuple to denote the number of tokens produced by this tuple This one must be a numeric expression statically evaluable and positive 28 CHAPTER 1 HELENA SPECIFICATION LANGUAGE complex tuple x tuplefor tuple guard tuple factor tuple tuple for ze for iteration scheme tuple guard Cif expression tuple factor expression x tuple ze 7 non empty expression list gt epsilon 1 2 11 State propositions Most properties are expressed by means of state propositions A state proposition is a boolean expression that usually refers to the current state using iterators see Section 1 2 9 16 A proposition has a name mean
42. bles transition bound variables transition bound variable Guard transition guard guard definition Priority transition priority Safe attribute safe hug Description transition description priority arc label pick free variable y free variable name in free variable domain type name range expression let transition bound variable y expression type name variable name guard guard definition expression expression 2 9 45 description string 1 non empty expression list A 1 NET SPECIFICATION LANGUAGE Expressions expression gt expression enumeration constant predecessor successor operation comparison operation function call if then else structure component vector assignment list list assignment list concatenation empty set set membership token component iterator expression list non empty expression list non empty expression list expression C expression Numerical and enumeration constants numerical constant xe number enumeration constant x name Predecessor and successor operators predecessor successor operation x pred expression succ expression Integer arithmetic integer operation
43. buted database system We consider in this system a set of N database managers which communicate to maintain consistent replica of a database It is a well known and recurrent example of the colored Petri nets literature initially presented by Genrich and later by Jensen When a manager updates its local copy of the database he sends requests to other managers for updating their local copy transition Update As soon as a manager receives such a request transition Receive he starts the update of its copy Its update finished each manager acknowledges the initiating manager transition Send ack This process finishes when the initiating manager collects all the acknowledgments transition Receive acks Managers can be either Inactive either Waiting for acknowledgments either Performing an update Places Msgs Received Acks and Unused model communication channels between sites Thus N N 1 tokens are distributed upon these places at each marking At last the correctness of the protocol is ensured by place Mutex which guarantees that two managers cannot concurrently update their local copy Lrep s s r A s r Receive type D is 1 N seD reD mo Mutex mo Inactive Esep s mo Unused X cpi zs 5 7 Send ack 5 r as s r Figure 3 1 The distributed database system Listing 3 1 Helena file of the distributed database system fil
44. call is the same as in the C language If the function does not take any parameter must follow the function name The type of the expression is the return type of the function The parameters passed to the function must fit with the function declaration the number of parameters must be the same in the declaration and in the call and the type of each parameter must be the same type as in the declaration The value of the expression is the value returned by the function for the parameters specified function call function name expression list 1 2 9 8 Cast Type casting allows to convert a value of any discrete type to another type The source and target types must have at least one value in common Errors will be raised at the run time if the cast fails i e the value of the casted expression does not belong to the type in which the expression is converted cast x type name expression 1 2 9 9 If then else The if then else expression taken from the C language is allowed in Helena An if then else consists in a boolean condition and two expressions which must have the same type The condition is evaluated If it is evaluated to true the resulting ex pression is the first expression Else it is the second one The resulting expression has the type of the true and false expressions if then else condition true expression false expression condition ze expression
45. ccept predicate predicate uz Cdeadlock state proposition name Temporal properties temporal property ve o Cltl property property name temporal expression temporal expression x temporal expression true false state proposition name not temporal expression temporal expression temporal expression temporal expression and temporal expression 11 temporal expression lt gt temporal expression temporal expression until temporal expression 66 APPENDIX A SYNTAX SUMMARY Gnu general public license Version 2 June 1991 Copyright 1989 1991 Free Software Foundation Inc 59 Temple Place Suite 330 Boston MA 02111 1307 USA Everyone is permitted to copy and distribute verbatim copies of this license document but changing it is not allowed PREAMBLE The licenses for most software are designed to take away your freedom to share and change it By contrast the GNU General Public License is intended to guarantee your freedom to share and change free software to make sure the software is free for all its users This General Public License applies to most of the Free Software Foundation s software and to any other program whose authors commit to using it Some other Free Software Foundation software is covered by the GNU Library General Public License instead You can apply it to your programs too When w
46. ce 23 structure operation 20 structure assignment 20 structure component 20 structure constructor 20 token component 23 variable 18 vector operation 21 vector assignment 21 vector component 21 vector constructor 21 71 function 15 iteration scheme 17 26 27 net 8 net parameters 8 place 11 capacity 12 domain 12 initial marking 12 type 12 state properties 28 state propositions 28 statement 15 assertion 17 assignment 16 block 16 case 16 for loop 17 if then else 16 return 16 while 16 subtype 10 temporal properties 29 transition 13 arc 13 bound variables 14 description 15 free variable 13 guard 14 priority 14 safe attribute 14 type 9 enumeration type 10 list type 10 modulo type 9 range type 9 set type 10 structured type 10 vector type 10
47. d Its visibility terminates with the end of the block A variable declared in the block hides previously declared variables with the same name block u 74 declaration statement y declaration xe constant declaration variable declaration type name variable name expression name variable declaration variable name 1 2 8 6 While Helena s while statement has exactly the same semantic as C s while statement as long as the boolean expression is evaluated to true the enclosed statement is executed while statement vihile expression statement 1 2 NET SPECIFICATION LANGUAGE 17 1 2 8 7 For loop A for statement iterates on all the possible values of some variables called the iteration variables Iteration variables are implicitly declared with the for statement Thus if another variable with the same name has been previously declared it is hidden in the for statement In addition iteration variables are not visible outside the for statement and they are considered as constant in the enclosed statement The domain of an iteration variable is evaluated once before entering the loop Thus even if the bounds depend on some variable which value is changed in the for it will have no consequence on the iteration We will call iteration scheme a list of iteration variables These schemes appear in for loops in iterators see Sec tion 1 2 9 16 or i
48. e an enabled transition execute it and reiterate this process The walk is reinitiated each time a deadlock state is met If no limit is specified see Section 2 1 4 the search will last forever t N hash size N Set the size of the hash table which stores the set of reachable markings to 2 The default value is 22 WzN workers N Specify the number of working threads that will perform the search This option is only usable if the search algorithm is DELTA DDD or RWALK cs N candidate set size N Set the cache size of algorithm DELTA DDD 100 000 is the default value Increasing it may consume more memory but can fasten the search 2 1 3 Reduction techniques H hash compaction The hash compaction storage method is used Its principle is to only store a hash signature of each visited state In case of hash conflict Helena will not necessarily explore the whole state space and may report that no error has been found whereas one could exist P partial order Specify if partial order reductions are applied during the search Partial order methods try to alleviate the state explosion problem by limiting the exploration of multiple paths that are redundant with respect to the desired property This causes some states to be never explored during the search The reductions done depend on the property verified If there is no property checked the reduction done only preserves the existence of deadlock states D delta This o
49. e An imported function must terminate This guarantees that the search also does e An imported function must be deterministic If the function is not Helena is not guaranted to report the same result across different executions The only exception is for functions that are used only once for the initialization of some net constant s The value of a constant may for instance be read from a file or from user inputs Note that all files accessed in imported functions must necessarily be accessed via an absolute path In addition it must also hold that for each imported function func in the net description there is in imported module s a function IMPORTED FUNCTION func such that its parameter and return types match with the declaration of function func in the net description Chapter Help 5 1 Evaluation of Transitions Helena puts some restrictions on the variables of transitions in order to be able to efficiently compute enabled transition bindings at a given marking Besides the fact that all variables of a transition have to be declared by appearing in a tuple labelling its input or inhibitor arcs or otherwise in the pick section additional constraints are put on these variables We summarize below the evaluation process in two situations when the transition does not have inhibitor arcs and when it does 5 1 1 Evaluation in the absence of inhibitor arcs During the computation of the enabled bindings of a transition that does not have an
50. e analyzed using the helena graph tool see Section 2 3 2 e CHECK prop Helena checks whether or not property prop which must be a property defined in the model file is verified property file FILE NAME File FILE NAME contains the definition of the property to check specified with option action CHECK prop By default if the input file of the model is model 1na Helena will try opening file model prop lna to look for the property definition md model directory DIRECTORY All generated files such as source files are put in directory DIRECTORY instead of helena models lna my net 2 1 2 Search options A ALGO TYPE algo ALGO TYPE This option is used to indicate to Helena the type of search that must be used to explore the state space Five search modes are available They correspond to the three following possible values for parameter ALGO TYPE e DFS The state space is explored using a depth first search This is the default e BFS The state space is explored using a breadth first search e FRONTIER The state space is explored using a breadth first search but only the states of the current level are kept in memory This algorithm will not terminate if the state space contains cycles e DELTA DDD The state space is explored using a parallel breadth first search based on state compression e RWALK Helena explores the state space using a random walk The principle is to randomly select at each stat
51. e empty list Two lists may be concatenated using the binary amp operator One of its operands must have a list type 1 which is also the type of the resulting expression The other operand must have the type or the element type of 1 Here are some examples of concatenations with the value of the resulting expression 11 2 3 41 amp 5 l 2 3 4 l 1 amp ill 2 31 amp 5 l 1 2 3 51 11 2 31 amp 14 5 l 11 2 3 4 5 l The concatenation of two lists may raise an error if the number of elements of the resulting list exceeds the capacity of the corresponding list type It is possible to check if an item belongs to a list by using the in operator For instance 5 in Il 2 51 true 2 in l 5 2 51 true 3 in l 51 false The resulting expression has the bool type The expression e in 1 is evaluated to true if there is an index i such that 1 i e or false otherwise Lastly list have some attribute that may be useful We can for example extract the prefix or the suffix of a list or select the first element of a list List attributes are described later in Section 1 2 9 15 1 2 NET SPECIFICATION LANGUAGE 23 empty list empty list xe 7 non empty expression list list component xe variable Y list assignment 2 U 2 3578 expression expression 1 expression list slice xe expression D expressio
52. e examples dbm 1na Z k k k k k k k k k k k k k k k k k k k k k k kk R CCCI SR R SR SR SR eee ee k k k ok k k k k k k ok k k dk x Example file of the Helena distribution 37 Qo 1 o Un 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 File dbm lina Author Sami Evangelista Date 27 oct 2004 Source Coloured Petri Nets A high Kurt Jensen If symbol UNUSED is defined In Application and Theory of Petri Nets the model CHAPTER 3 EXAMPLES level language for system p 342 416 Springer design and analysis 1989 includes the place unused os OR R xe R HE EE cee eS eee eee ee ee DH he HE EEE RD PR OO ee dbm N 10 x type site_id mod N Le process places modelling the x place inactive dom site id init for s in capacity 1 type process place waiting dom site_id capacity 1 type process place performing dom site_id capacity 1 type process places place sent dom site id capacity 1 type buffer site_id place received dom site id capacity 1 type buffer site id place acks dom site id
53. e in the most ordinary way to print or display an announcement including an appropriate copyright notice and a notice that there is no warranty or else saying that you provide a warranty and that users may redistribute the program under these conditions and telling the user how to view a copy of this License Exception if the Program itself is interactive but does not normally print such an announcement your work based on the Program is not required to print an announcement These requirements apply to the modified work as a whole If identifiable sections of that work are not derived from the Program and can be reasonably considered independent and separate works in themselves then this License and its terms do not apply to those sections when you distribute them as separate works But when you distribute the same sections as part of a whole which is a work based on the Program the distribution of the whole must be on the terms of this License whose permissions for other licensees extend to the entire whole and thus to each and every part regardless of who wrote it Thus it is not the intent of this section to claim rights or contest your rights to work written entirely by you rather the intent is to exercise the right to control the distribution of derivative or collective works based on the Program In addition mere aggregation of another work not based on the Program with the Program or with a work based on the Program on a volume
54. e speak of free software we are referring to freedom not price Our General Public Licenses are designed to make sure that you have the freedom to distribute copies of free software and charge for this service if you wish that you receive source code or can get it if you want it that you can change the software or use pieces of it in new free programs and that you know you can do these things To protect your rights we need to make restrictions that forbid anyone to deny you these rights or to ask you to surrender the rights These restrictions translate to certain responsibilities for you if you distribute copies of the software or if you modify it For example if you distribute copies of such a program whether gratis or for a fee you must give the recipients all the rights that you have You must make sure that they too receive or can get the source code And you must show them these terms so they know their rights We protect your rights with two steps 1 copyright the software and 2 offer you this license which gives you legal permission to copy distribute and or modify the software Also for each author s protection and ours we want to make certain that everyone understands that there is no warranty for this free software If the software is modified by someone else and passed on we want its recipients to know that what they have is not the original so that any problems introduced by others will not reflect on the original auth
55. ed to perform integer arithmetic the binary and 96 modulo operators and the unary and operators In the case of a binary operator both operands must be of the same type Let t be the type of the operand s The type of the resulting expression will also be t Its value depends on t e If t is a range type the expression has the conventional meaning A division by 0 will raise an error e If t is a modulo type the operation is done as for a range type The resulting value is then normalized as follows Let m be the modulo value of the type and r be the result of the operation If r is positive or zero the value of the resulting expression is r mod m If it is negative the result is r 4 m 1 r m mod m A division by also raises a run time error integer operation expression expression expression expression expression x expression expression expression expression expression 4 expression expression 1 2 9 5 Comparison operators The comparison operators and are defined for any type e For discrete types the equality test is straightforward e Two structured expressions are equal if all their corresponding components are equal Two vectors are equal if they contain the same elements at the same indexes e Two lists are equal if 1 they have the same length and 2 they contain the same elements at the same indexes e Tw
56. eive balancer_foute balancer no balance balancer balince Y server receive c client ack sc c Oe lt s c gt server_send Figure 3 2 The whole load balancing system In this system we have two kinds of process a set of clients and a set of servers An additional process called the load balancer distribute requests of clients to servers Its task is also to redistribute pending requests when servers accept requests in order to maintain the loads of servers balanced The clients We note C the number of clients considered Clients are numbered from 1 to C The behavior of the clients is quite simple A client may want to send a request to a set of servers Instead of asking a server directly he sends the request to the load balancer which will route the request to the adequate server 1 e the least loaded server Once the request sent the client waits for the answer When this one arrives the client comes back to the idle state The servers The number of servers is noted S Servers are numbered from 1 to S Servers receive requests from clients via the load balancer process When a server accepts a request he first has to notify this to the load balancer process in order that this one rebalances the pending requests Then he has to wait for an acknowledgment from the load balancer to start treating the request Once the request treated he directly sends the answer to the concerned client and goes back to the id
57. ement at index false true vector x 12 non empty expression list 1 vector component variable non empty expression list 1 vector assignment expression C non empty expression list expression 22 CHAPTER 1 HELENA SPECIFICATION LANGUAGE 1 2 9 12 Lists Lists can be handled in the same way as vectors and structures We will illustrate the different possibilities with the help of the type int_list defined below type int_list list nat of int with capacity 10 First we can construct the empty list 1 e that does not contain any element with the help of the keyword empty as in the example below constant int_list empty_list empty A list can also be constructed by placing all its elements between two characters For example constant int list 1 Il 2 3 4 51 The list l is a list of five integers Its element at the first index is the constant 1 At the second index there is the constant 2 and so on The elements of a list can be accessed via their indexes as for vectors For example if we consider the list 1 previously defined 1 0 will be the first element of the list i e 1 1111 the second element of the list and so on An error will be raised if we attempt to access an element at an index that does not exist e g 1 5 Let us note that the classification starts at O since the index type of int_list is nat If this index
58. en cyanl of type colorList is equivalent to a C expression red ex items 0 TYPE ENUM CONST color green ex items 1 TYPE ENUM CONST color ex items 2 TYPE ENUM CONST color cyan ex length 3 the value of ex items 3 and ex items 4 are irrelevant e A sub type is simply translated to its parent type 4 2 2 Generated constants and functions It may be useful for the user to access in imported modules the values of some constant s or the function s declared in the net specification Hence each constant or function is also accessible in the header file generated by the helena generate interface tool An example of translation is provided by Table 4 2 The mapping is straightforward We simply notice that an Helena constant const is mapped to a C variable CONSTANT_const and that an Helena function func is mapped to a C function FUNCTION_func In addition the parameter and return types of the Helena function and the C function must match 4 3 Requirements on imported modules Imported functions must fulfill some requirements so that it does not impact negatively on the behavior of Helena These are listed below e An imported function may not have any side effect In particular it is absolutely necessary that the function frees all memory it allocates Otherwise since the function will be called multiple times during the search memory could be quickly saturated
59. esired property is verified or not In the second case a path leading from the initial marking to the faulty marking is displayed Each option has a short form preceded by a single and a long form preceded by Most options take an argument To invoke Helena on a file my net 1na with an option opt having argument arg simply type helena opt arg my net lna In addition let us note that the options are interpreted in the order in which they are found Hence in case of conflicting options the last ones will prevail 2 1 1 General options h help Prints a help message and exit V version Prints the version number and exit v verbose This option activates the verbose mode Helena prints a message at each step N action ACTION This indicates the action performed by Helena on the model ACTION must have one of the following values e EXPLORE Helena explores the state space of the model and then prints some statistics This is the default 31 32 CHAPTER 2 USING HELENA e SIMULATE Starts helena in interactive simulation mode You can then navigate through the reachability graph of the model by executing transitions undoing transitions A simple command language is provided Once the simulation is started type help to see the list of commands e BUILD GRAPH Helena builds the reachability graph of the model using a search algorithm DELTA DDD see option algo and store it on disk This graph can then b
60. gcc c isSorted c We can now invoke Helena with option 1 in order to specify which object files must passed to the linker helena L initList o L quickSort o L isSorted o actionecheck not dead sort lna Helena automatically compiles C files generated for the net file sort 1na and link them with files initList o quickSort o and isSorted o After the search is completed we can see a simulation of the quick sort algorithm for the simple list returned by function initList myList lt 14 1 3 0 21 1 gt T 12 14 1 3 21 steps 11 myList 12 1 3 0 41 2 gt 0 1 12 1 3 41 steps 21 gt i myList lt 12 1 0 3 41 3 gt 12 12 1 0 3 4l steps 3 myList 10 1 2 3 4l 4 gt 4 2 The interface file As shown in our tutorial the helena generate interface tool must be invoked in order to generate an header file contain ing the C code that could be required to implement imported modules The purpose of this section is to describe exactly the content of this header file 4 2 1 Generated types The Table 4 1 contains for each kind of type or sub type in the Helena net the corresponding C type that is generated The translation is pretty straightforward We can however make the following comments e Each Helena type or sub type t is mapped to a C type TYPE t e A numeric type is mapped to type short or int depending on its range of values The same applies
61. he vector i e the length of the expression list in the vector is less than the number of elements of the vector type the last expression in the vector is used for the non specified elements Let us consider for instance the following vector type declaration type bool_matrix vector bool bool of bool and the following variable declaration constant bool_matrix ml false false true constant bool_matrix m2 false The vector m1 and m2 will be defined by ml false false ml false true false ml true false ml true true true m2 false false m2 false true n2 true false m2 true true false Let us recall that the predefined type bool is defined as type bool enum false true Secondly a specific element of a vector can be accessed Let us consider the type bool matrix previously defined and m a variable of this type The expression m false false is a boolean expression i e the type of the elements of vector type bool matrix and its value is the value of the element of m which index is false false At last an element of a vector can be assigned an expression The syntax is close to the syntax of a structure assign ment Instead of specifying the name of a component an index of the vector is supplied For instance the expression m true false m false true has the same type as m Its value is the vector m in which the element at index true false has been replaced by the el
62. ial type of error since they are not detected at the evaluation of sub expressions but at the whole expression evaluation Let us consider for instance the following type declaration type my_type range 1 10 my_type i The expression i 1 gt 1 will never raise an error even if i has value 1 since the whole expression is correct However the statement i i 1 will raise an error if i 1 since the final expression is out of the range of type my_type expression n expression numerical constant expression list non empty expression list enumeration constant predecessor successor operation comparison operation function call if then else structure component vector vector assignment list list assignment list concatenation empty set set membership token component iterator E non empty expression list expression C expression 1 2 9 1 Numerical and enumeration constants variable integer operation boolean operation cast structure structure assignment vector component empty list list component list slice list membership set set operation attribute A PS Constants are the most basic expressions The resulting expression has the value of the constant For a numerical constant the resulting expression is of any integer type range or modular which greatest bound in absolute value is greater than the constant
63. ion has an undefined value Iterators sum and product compute respectively a sum and a product The expression inside the iterator can have any numerical type which is also the type of the resulting expression e Iterator card computes the number of iterations that fulfill a condition No expression must be provided in the iterator The resulting expression can have any numerical type e Iterator mult is only valid if a single iteration variable is provided and if its domain is a place It computes the sum of the multiplicities of the tokens in this place which fulfill a condition No expression must be provided in the iterator The resulting expression can have any numerical type We illustrate the use of these iterators on several examples Let t be the type and p be the place defined by type t range 1 10 place p dom t bool The marking of place p at the current state is given by the following tokens distribution l true 2x lt 2 false gt lt 2 true gt 3x lt 4 true gt 4x lt 8 false gt Let us detail the evaluation of some iterators e exists t in p true Indeed there are five tokens in place p forall t in p t gt 2 t gt 1 lt 5 true All the tokens in place p which have their second component equal to true have their first component strictly less than 5 e card t in p not t gt 2 2 There are 2 tokens in place p which have their second component equal to false e mult t in p
64. is License to do so and all its terms and conditions for copying distributing or modifying the Program or works based on it Each time you redistribute the Program or any work based on the Program the recipient automatically receives a license from the original licensor to copy distribute or modify the Program subject to these terms and conditions You may not impose any further restrictions on the recipients exercise of the rights granted herein You are not responsible for enforcing compliance by third parties to this License If as a consequence of a court judgment or allegation of patent infringement or for any other reason not limited to patent issues conditions are imposed on you whether by court order agreement or otherwise that contradict the conditions of this License they do not excuse you from the conditions of this License If you cannot distribute so as to satisfy simultaneously your obligations under this License and any other pertinent obligations then as a consequence you may not distribute the Program at all For example if a patent license would not permit royalty free redistribution of the Program by all those who receive copies directly or indirectly through you then the only way you could satisfy both it and this License would be to refrain entirely from distribution of the Program If any portion of this section is held invalid or unenforceable under any particular circumstance the balance of the section is in
65. k k k ke ICI I k II Gk SR k k 4 Example file of Helena distribution File 34 s0rt in Author Sami Evangelista Date 3 mar 2010 This simple example illustrates the use of imported functions informations on this model Please read the user s guide in directory doc if you want more To analyse this net you must first compile the C imported functions and then invoke helena as follows x gt helena generate interface sort lna sort interface h gt ACC Eni List xe quickSort o issorted e gt helena L initList o L quickSort o L isSorted o sort ina kA K R EEE ee od ode R a a KEk sort type intList list nat of int with capacity 1000 function initList gt intList function quickSort intList 1 int steps gt intList function isSorted intList 1 gt bool 47 48 CHAPTER 4 INTERFACING HELENA WITH C CODE constant intList toSort initList place myList dom intList int init lt toSort 1 gt transition swap in myList lt 1 steps gt out myList quickSort toSort steps steps 1 gt guard not isSorted 1 import function initList gt intList import function quickSort intList 1 int steps gt intList import function isSorted intList 1 gt bool The transition swap is only firable if the list taken in place myList is not already sorted The v
66. k based on the Program independent of having been made by running the Program Whether that is true depends on what the Program does You may copy and distribute verbatim copies of the Program s source code as you receive it in any medium pro vided that you conspicuously and appropriately publish on each copy an appropriate copyright notice and disclaimer of warranty keep intact all the notices that refer to this License and to the absence of any warranty and give any other recipients of the Program a copy of this License along with the Program You may charge a fee for the physical act of transferring a copy and you may at your option offer warranty protection in exchange for a fee You may modify your copy or copies of the Program or any portion of it thus forming a work based on the Program and copy and distribute such modifications or work under the terms of Section 1 above provided that you also meet all of these conditions a You must cause the modified files to carry prominent notices stating that you changed the files and the date of any change b You must cause any work that you distribute or publish that in whole or in part contains or is derived from the Program or any part thereof to be licensed as a whole at no charge to all third parties under the terms of this License c If the modified program normally reads commands interactively when run you must cause it when started running for such interactive us
67. l others are empty place towers dom tower disk list init tower first construct towerl for t in tower range tower first 1 tower last t empty transition move disk models the move of the disk on top The description is taken from http en wikipedia org wiki Tower of Hanoi 44 45 46 47 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 WN 46 CHAPTER 3 EXAMPLES of tower src to the tower dest the src stack must not be not src disks empty if the dest tower is not empty the disk on top of src src disks last must be smaller than the disk on top of the dest tower dest disks last the move consists of deleting the last element from the src stack src disks prefix is the the list src disks from which we remove the last element and pushing it onto the dest stack transition move disk in towers src src disks dest dest disks gt out towers remove the last disk of tower t lt src src_disks prefix gt add the removed disk on top of tower u lt dest dest disks amp src disks last gt guard not src disks empty and dest disks empty or src disks last dest disks last description move disk d from tower 58 to tower 3d src disks last src dest in the end state the last tower is full i e
68. le state The load balancer The load balancer can perform two kinds of task The first one is to redirect each client request to the least loaded server Secondly when a server accepts a request from a client the load balancer has to rebalance the pending requests If these are already balanced the load balancer has nothing to perform and can come back to its idle state transition balancer_no_balance If the loads are not balanced the load balancer takes a pending request of the most loaded server and redirects it to the least loaded server transition balancer balance The load balancer has to maintain for each server the number of requests sent to this server 00 1O0 t i Q2 QN a Un GA Un CA Un Un Un Un CA d amp RR RR UR RR dA dA 4 Lo LI U LI LI Lo LW C9 WI t R RD TO RD R NN nom S a A D d X160 D D 00 X30 D D 1 Ur OI EAN t RU D O vo 3 2 THE LOAD BALANCING SYSTEM 41 Listing 3 3 Helena file of the load balancing system file examples load_balancer 1na k 3k EEE SESE LEE SR SEES EE HELE SPREE SEER REESE x Example file of the Helena distribution File load balancer lna Author Sami Evangelista Date 27 oct 2004 This file contains the description of a load balancing system k k 9 SR SR R SR k k k k k sk k k k k k kk k k k ee ee ee ee ee k k sk k k eee ee ee I
69. lena constructions that are identified by textual names or identifiers Identifiers must start with an alphabetic character and must only contain alpha numeric characters or the _ character They also must of course not belong to the list of reserved words 1 1 1 3 Numerical constants A valid numeric constant has the form 0 9 0 9 Octal or hexadecimal notations are not allowed The maximal constant allowed is system dependant but is 23 on most systems 1 1 1 4 Comments Comments are indicated as in the C language Two slashes start a comment that will end with the current line start a comment which is explicitely ended by x Comments can not be nested 11 2 Preprocessor directives Helena features some preprocessor directives taken from the C language However it must be noticed that preprocessor symbols are not macros Thus no expansion takes place A directive starts with a at the first column followed by a list of blanks possibly empty and followed by the directive name 8 CHAPTER 1 HELENA SPECIFICATION LANGUAGE 1 1 2 1 Defining and undefining symbols Symbols can be defined and undefined by directives define and undefine The directive must be followed by the symbol name A symbol name must be a valid identifier possibly a reserved word 1 1 2 2 Conditional compilation Directives ifdef ifndef else and endif can be used for conditional compilation Directive ifdef checks if the symbol placed just
70. mpty set non empty expression list set membership x expression in expression set operation xe expression or expression expression and expression expression expression 1 2 9 14 Token component Iterator expressions can be used to iterate on the tokens present in a place at the current marking To check complex conditions on these tokens components of tokens can be accessed by specifying the name of the token variable followed by symbol and the number of the accessed component of the token type For instance let us consider the following place definition place p dom int bool x int If the type of variable t is the token type of place p then t 1 t gt 2 and t gt 3 are three valid expressions t 1 and t gt 3 have both type int while t 2 has type bool t gt 4 is not a valid expression since the domain of place p is a product of three items token component number variable name number token component token component number 1 2 9 45 Attributes Some elements have attributes that can be used in expressions The syntax of an attribute is inherited from the Ada syntax it consists of the element e g a type name a place name followed by the character and the name of the attribute Table 1 1 summarizes the possible attributes and their meaning There are several categories of attributes 24 CHAPTER 1 HELENA SPE
71. n 1 list concatenation x expression expression list membership expression in expression 1 2 9 13 Sets Some constructions are common for sets and lists For example it is possible to construct an empty set with the help of the empty keyword A set can also be defined by placing all its elements between two characters Set membership is realized through the in operator as for lists The or and and operators may be used to compute the union intersection and differences of two sets One of the operands of these operators must be a set while the other can be a a set of the same type or an expression of the element type of the set A run time error will naturally be raised if the cardinal of the resulting set exceeds the capacity of its type At last lists and sets have many attributes in common You will find a complete list of these attributes at Section 1 2 9 15 Let us examine some examples that illustrate the use of sets type int_set set of int with capacity 10 constant int set sl 11 2 31 constant int set s2 1 2 3l or 12 3 4l 52 11 2 3 41 constant int set s3 1 2 31 and 12 3 41 53 I2 31 constant int set s4 0 or l 21 or 5 Jf 44 eL 11 7 SI constant int set s5 11 2 31 11 21 If so NS constant int set s6 Il 2 31 1 gs6 18 51 constant bool b 3 in sl Ar Ibo TUE constant bool c 4 in sl e false empty set e
72. n front of tuples that label the arcs see Section 1 2 10 2 of the net The domain of an iteration variable v can be e a discrete type t The iteration variable successively takes all the values of t from the first one to the last one The iteration may be limited to a specific range The type of the iteration variable is t e a place p In this case all the tokens present in the place at the current state will be considered The type of the iteration variable is the token type of p the different components of the token may then be accessed using the syntax v gt 1 e a container c that is any expression which has a set or a list type In this case all the items in the container will be considered If the container is a list it will be traversed from the first element to the last If 1t is a set no assumption can be made on the order of traversal The type of the iteration variable is the element type of the type of c In the case of for loops place iteration variables are not allowed In the following example we define a function compute_sum which computes the sum of some integers contained in a set type int_set set of int with capacity 10 function compute_sum int_set s gt int int result 0 for item in s result result item return result for statement xe for iteration scheme statement iteration scheme iteration variable iteration variable iteration variable variable name
73. name type definition subtype name range type type um modulo type type name type definition enumeration type vector type struct type list type set type 1 2 8 4 Range type A range type is an integer type which values belong to a specified range A range type is defined by specifying the lower bound and the upper bound of the range Bounds must be numerical expressions statically evaluable see Section 1 2 9 for more precisions on statically evaluable expressions Additionally the upper bound of the type must be greater or equal to the lower bound The integer type int is a predefined range type Its definition is system dependant but on most systems it is defined as follows type int range 2147483648 2147483647 range type x range range xe range expression expression 1 2 3 2 Modulo type A modulo type is an integer type which values can range from 0 to m 1 where mis a specified value called the modulo value This one must be a numerical expression statically evaluable and strictly positive modular type mod expression 10 CHAPTER 1 HELENA SPECIFICATION LANGUAGE 1 2 3 3 Enumeration type An enumeration type consists in a non empty collection of distinct enumeration constants The boolean type bool is a prede fined type which is defined as type bool enum false true It will be referred in the remainder a
74. nce from the user some informations can be put in the specification in order to guide Helena into the search and optimize some of these techniques We detail now these features 5 3 Guiding Helena in the search Some informations provided by the user are not mandatory but given to Helena in order to make its search more efficient However Helena does not have any mean to check the validity of the informations provided Thus if some of these revealed to be erroneous Helena could produce wrong results e g report that a property is verified whereas it is not We therefore encourage users to be very careful when supplying these informations and to ignore them if there is any doubt regarding their validity 5 3 1 Typing places A type can be associated to each place of the net This type specifies the nature of the information modeled by the place The types provided allow to model concurrent systems and protocols synchronizations through shared variables and communica tion buffers Six kinds of places are allowed process places local places shared places protected places buffer places and ack places Process places Figure 5 1 top left Process places model the control flow of processes i e its position in the code it executes A process is therefore in exactly one of the process places of the net The simple net depicted models cyclic process Each process p can go from state Idle to state Working Thus for each process p there is a token
75. nd installation of the executable However as a special exception the source code distributed need not include anything that is normally distributed in either source or binary form with the major components compiler kernel and so on of the operating system on which the executable runs unless that component itself accompanies the executable If distribution of executable or object code is made by offering access to copy from a designated place then offering equivalent access to copy the source code from the same place counts as distribution of the source code even though third parties are not compelled to copy the source along with the object code You may not copy modify sublicense or distribute the Program except as expressly provided under this License Any attempt otherwise to copy modify sublicense or distribute the Program is void and will automatically terminate your rights under this License However parties who have received copies or rights from you under this License will not have their licenses terminated so long as such parties remain in full compliance You are not required to accept this License since you have not signed it However nothing else grants you permission to modify or distribute the Program or its derivative works These actions are prohibited by law if you do not accept this License Therefore by modifying or distributing the Program or any work based on the Program you indicate your acceptance of th
76. not in r Transition u is firable for some binding x if and only if the token lt x gt is present in p and there exists no y such that the token lt x y gt is present in s Note that variables defined in inhibitor arcs are not variables of the transition For example variable y of transition u serves only during the evaluation of the transition 5 2 Tips and Tricks This section gives some hints to use Helena in an efficient way Saving memory Helena provides some predefined data types However we encourage users to define application specific data types in order to limit the possible values of variables and to save memory when markings are stored in the reachability set Let us consider for instance a place with domain int Each token of this place will be encoded in a marking with 32 bits However if we know that the tokens of this place can only belong to the range 0 50 it is preferable to define a new range type ranging from 0 to 50 Thus tokens will fit in 6 bits instead of 32 If you are not sure of this range use option run time checks to detect expressions going out of range For the same reason try to limit capacities of places Option run time checks will also detect violated capacities Storage methods We advise to proceed as follows when verifying a property e Use a partial search with hash compaction method option hash compaction This method can explore a large portion of the state space and report errors much
77. nterpretation e capacity e is a container the capacity of e e card e is a discrete type the cardinal of e e is a place the number of distinct tokens in e e empty e is a container e is empty e first e is a discrete type the first value of e e is a list the first element of e e first index eis a list the index of the first element of e e prefix e is a list the first elements of e e full e is a container the capacity of e is reached e last e is a discrete type the last value of e e is a list the last element e e last_index eis a list the index of the last element of e e suffix e is a list the last elements of e e length e is a list the length of e e mult e is a place the cumulated multiplicities of the tokens in e e space e is a container the remaining space in e List attributes Let 1 be a list i e an expression of which the type is a list type t defined as type t 1 first is the first element of 1 The type of this expression is element type A run time error is raised if 1 is empty 1 last is the last element of 1 The type of this expression is element type A run time error is raised if 1 is empty list index type of element type with capacity N 25 1 prefix is the list which consists of the first elements of 1 i e the list 1 from which we remove the last element The type of this expression is t A run time error i
78. o The transition Take is clearly not safe Indeed each enabled binding Take p o needs a token o in place Objects and this token can be removed by any other process q which wishes to acquire the same object Thus Take q 0 disables Take p o Let us now have a look at transition Release Once the binding Take p o is fired there is a token p in place Working and a token p o in place Taken Since p is the only process which can remove token p o from place Taken the transition binding Release p o is safe This obviously holds for any process p and object o Consequently we can declare transition Release as safe 58 CHAPTER 5 HELP Appendix Syntax summary A 1 Net specification language Nets net net name definition Net parameters net parameter list net parameter net parameter name Types and subtypes type type name type definition Range type range type range Modulo type modular type net name net parameter list 1 U definition y name type constant function place transition state proposition net parameter net parameter net parameter list net parameter name number name 8 uus type name type definition subtype name range type modulo type enumeration type vector type struct type list type set type
79. o sets are equal if they contain the same elements The operators gt gt and lt are only defined for discrete and set types e For integer types the comparison is straightforward e Enumeration types are ordered according to the way the type has been declared For instance let us consider the following declaration type color enum red green blue It follows from the declaration that red lt green blue e For set types it holds that sl gt s2 if and only if the set s2 is a strict subset of the set sl A comparison operation has the boolean type comparison operation expression expression expression 1x expression expression 75 expression expression gt expression expression lt expression expression expression 20 CHAPTER 1 HELENA SPECIFICATION LANGUAGE 1 2 9 6 Boolean logic Boolean connectors are essential to express complex boolean expressions used for example in transition guards The lan guage includes the classical or and and not operators The operand s of these operators must have the boolean type which is also the type of the resulting expression We thus forbid expression such as 1 or 0 which are allowed by the C language boolean operation x expression or expression expression and expression not expression 1 2 9 7 Function call Functions previously declared can be called The syntax of a function
80. of types called token types A token type is some kind of structured type which elements are given by the domain of the place A token type is hidden from the user and can thus not be used Token types are only used in iterators see Section 1 2 9 16 domain ze dom domain definition domain definition epsilon types product types product type name x type name 1 2 5 2 Initial marking The initial marking i e before the firing of any transition of a place can be defined in the place description Any valid arc label can be used to initialise the marking of a place 2 initial marking init marking marking arc label 1 2 5 3 Capacity We call the capacity of a place the maximal multiplicity of any item in this place In the formal definition of Petri nets this capacity is infinite However the amount of available memory being finite an implementation must fix this one The capacity specified must be a numerical expression statically evaluable and strictly positive Errors can be raised at the run time if the supplied capacity is not sufficient 9219 gt capacity capacity expression 1 2 5 4 Type A type can be associated to each place of the net This type specifies the kind of information which is modeled by the place Several types are allowed Process places model the control flow of processes Local places model resources local to a proces
81. ors reputations Finally any free program is threatened constantly by software patents We wish to avoid the danger that redistributors of a free program will individually obtain patent licenses in effect making the program proprietary To prevent this we have made 1t clear that any patent must be licensed for everyone s free use or not licensed at all The precise terms and conditions for copying distribution and modification follow GNU GENERAL PUBLIC LICENSE TERMS AND CONDITIONS FOR COPYING DISTRIBUTION AND MODIFICATION 0 This License applies to any program or other work which contains a notice placed by the copyright holder saying it may be distributed under the terms of this General Public License The Program below refers to any such program or 67 68 APPENDIX B GNU GENERAL PUBLIC LICENSE work and a work based on the Program means either the Program or any derivative work under copyright law that 1s to say a work containing the Program or a portion of it either verbatim or with modifications and or translated into another language Hereinafter translation is included without limitation in the term modification Each licensee is addressed as you Activities other than copying distribution and modification are not covered by this License they are outside its scope The act of running the Program is not restricted and the output from the Program is covered only if its contents constitute a wor
82. p in place Idle or in place Working Local places Figure 5 1 top right Local places model resources local to a process Intuitively this means that two different processes cannot withdraw the same token from a local place The net depicted models the incrementation by 1 of a local variable 7 This variable is modeled by the place 7 The first component of the domain of this place is the identifier of the process which owns the local variable and the second one gives the value of this variable Since a process p can only access its own variable and withdraw a token of type p i from place J we can type this place as local Indeed two different process cannot currently consume the same token in place Shared and protected places Figure 5 1 bottom left Shared places model resources shared by processes Shared vari ables or locks are examples of informations which can be modeled by a shared place Protected places are special shared places They are used to model resources which can be accessed by several processes but which cannot be accessed concur rently thanks to a mechanism e g a mutex which guarantees that two processes cannot simultaneously access the resource The net depicted models the incrementation of a shared variable 7 To update the value of 7 a process must first grab a lock modeled by place Lock This lock ensures that two processes cannot concurrently update 7 We can thus declare 7 as protected The place Lock is naturally a
83. ption can activate the delta markings storage method to store the state space The basic idea is store a large set of states compactly by only storing differences with respect to others states of the state space This technique can greatly reduce the memory needed to store the state space but will also slow the search Option K can be set to influence this 2 1 INVOKING HELENA 33 K N k delta N This is the parameter of the delta markings storage method Consequently this has no effect if D 0 is passed to Helena The higher this parameter is the less memory will be needed to store the state space and the slower the search will be S state caching The principle of state caching is to only store a subset of visited states in such a way that termination is still guaranteed Other visited states are forgotten This technique can be very efficient but can also considerably increase the execution time by revisiting forgotten states s cache size N When using state caching Helena can keep some visited states in a cache in order to limit redundant state revisits This option is used to specify the size of this cache 2 1 4 Search limits ml N memory limit N The memory used by Helena is limited to N of the available RAM When this limit is reached the search stops as soon as possible tl N time limit N The search time is limited to N seconds When this limit is reached the search stops as soon as possible sl N state limi
84. ption is only meaningful if used in conjunction with the helena graph utility Let us assume that the file my net 1na contains the description of net my net A typical use of this combination is helena action BUILD GRAPH my net lna helena graph my net my_rg_report pdf e The first command explores the reachability graph of the net and stores it on disk in the model directory in helena by default e The second command reads this file and produces a report containing various informations on the graph e g in out degrees of nodes shape of the BFS level graph SCCs of the graph dead markings live transitions The output format of this report can be pdf or xml In the case of a pdf report you will need pdflatex as well as the Gnuplot python library on your system 2 3 3 The helena generate interface utility This tool is used to generate a C header file containing the translation of types constants and functions that can then be used in imported modules Please consult Chapter 4 for further help on this tool 36 CHAPTER 2 USING HELENA Examples In this section we illustrate the possibilities of our description language The first system studied is a distributed database system Then we describe a load balancing system which makes use of more advanced features of our tool The third example is the well known puzzle of the towers of Hanoi This one illustrates a use of high level data types provided by Helena 3 1 The distri
85. r binding If a transition is safe all its bindings are considered by Helena as safe Please report to Chapter 5 Section 5 3 for further details on this feature safe xc safe 1 2 6 6 Priority Transitions can be prioritized A valid priority is any expression of type int A transition may not fire for a given binding if another binding of the same or any other transition with a greater priority is also enabled By default the priority of any binding is O It is allowed to refer in a priority expression to all variables of the transition Moreover the priority system of Helena is dynamic in the sense that the content of a place may also be used to define a priority using e g iterators see Section 1 2 9 16 Hence the priority of a transition depends on the current system state Let us consider the following definitions transition t in q lt x out r x gt priority x 0 and p card gt 0 1 0 1 2 NET SPECIFICATION LANGUAGE 15 Then it follows that transition t has priority 1 for binding x 0 and if place p is not empty Otherwise it has priority 0 transition priority w priority expression 1 2 6 7 Description The default string printed by Helena to describe a transition may be replaced by providing a description This description consists of a formatting string following the C conventions followed by the expressions that may appear in this string All these expression
86. r specification C parameter specification parameter specification type name parameter name function name name parameter name xe name Statements statement x assignment if statement case statement while statement for statement return statement assert statement block Assignment assignment x variable expression A 1 NET SPECIFICATION LANGUAGE 61 If then else if statement if expression true statement else false statement true statement statement false statement statement Case case statement case expression case alternative default alternative 1 3 case alternative expression statement default alternative x default statement While while statement x while expression statement For loop for statement xe for iteration scheme statement iteration scheme iteration variable iteration variable iteration variable variable name in type name range variable name in place name variable name in expression Return return statement return expression Assertion assert statement assert Block block 41 declaration statement declaration ze constant declaration gt type
87. ree variable free variable name in free variable domain free variable domain type name range expression 1 2 6 3 Bound variables The let section of a transition declaration is provided to declare bound variables that are used to avoid repeating the same expression in the transition Note that bound variables are evaluated right after input arcs and free variables Hence they may not appear in these arcs or in the definition of free variables but can appear at all other places within the transition declaration in the output or inhibitor arcs in the guard and in the priority For instance the following declaration transition t in q lt x out r lt f x gt guard f x gt 0 if equivalent to transition t in q lt x gt out r lt y gt let int y f x guard y gt 0 transition bound variables x let 7 transition bound variable y transition bound variable type name variable name expression 1 2 6 4 Guard Transitions can be guarded by a boolean expression This guard is an additional condition that the variables of the transition must fulfill for a binding to be firable gt transition guard guard guard definition guard definition expression 1 2 6 5 Safe attribute Transitions can be declared as safe A transition binding is safe if it can not be disabled by the firing of any othe
88. s e g a local variable Shared places model resources shared by several processes of the system e g a global variable Protected places model shared resources which can not concurrently be accessed by the processes e g a global variable which is protected by a lock Buffer places model communication buffers between processes Ack places are special buffer places An ack place models an acknowledgment of a synchronous exchange between two processes Chapter 5 Section 5 3 gives more details on the use of this feature Remark Since it is usual to name places or transitions process local buffer we decided not to include these in the list of reserved words place type xe type place type name place type name process local shared protected buffer ack 1 2 NET SPECIFICATION LANGUAGE 13 1 2 6 Transitions Transitions of a Petri net are active nodes that may change the state of the system that is the distribution of tokens in the places Transitions need some tokens in their input places to be firable and produce tokens in their output places To further restrain the firability of a transition inhbitor arcs may be used to specify that some tokens must not be present in a specific place In high level Petri nets arcs between places and transitions are labeled by expressions in which variables appear Thus a transition is firable for a given instantiation or binding
89. s must be of discrete types Here is an example of transition description transition t in q lt x gt out r lt x b gt pick b in bool description move d from q to r x gt 53 transition description description string non empty expression list 1 2 7 Functions The user is allowed to define functions which may then appear in arc expressions or in the property to verify Functions can not have any side effect They are functions in the mathematical sense they take some parameters compute a value and return it Two alternatives are possible to write the body i e the effect of a function First it can be written in the language provided by Helena that is described bellow Second it is possible to import it from a C function that is to write it directly in C and then to invoke Helena with option L in order to link the appropriate object files This second alternative is described in Chapter 4 To allow the definition of mutually recursive functions the prototype i e name parameters and return type of the function must be specified before its own body The prototype and the body must naturally match A function becomes visible as soon as its prototype or body is declared function xe function declaration function body function prototype xe function function name C parameters specification gt type name function declaration
90. s raised if 1 is empty 1 suffix is the list which consists of the last elements of 1 i e the list 1 from which we remove the first element The type of this expression is t A run time error is raised if 1 is empty 1 first index is the index of the first element of the list It always hold that 1 first index index type first The type of this expression is index type 1 last index is the index of the last element of the list The type of this expression is index type A run time error is raised if 1 is empty Let us have a look at some examples type int_list constant int_ constant int constant int constant int_ constant int_ constant nat constant nat of int with capacity 10 list nat list 1 13 5 12 5 il 1 first 24 12 last list 11 1 prefix list 12 1 suffix nl l first index n2 l last index FE 101 5 10 11 13 5 12 5l I2 m 15 12 5 101 nl 0 n2 4 26 CHAPTER 1 HELENA SPECIFICATION LANGUAGE gt attribute type name type attribute place name place attribute expression container attribute expression list attribute type attribute ze first last card place attribute ze ecard mult container attribute full empty capacity size space list attribute se first first index prefix la
91. s the boolean type os enumeration type enum enumeration constant enumeration constant enumeration constant x name 1 2 3 4 Vector type Elements of a vector type or array type consist in a set of contiguous elements of the same type called the element type that may be accessed by specifying an index or more precisely a list of indexes These indexes must be of discrete types The number of elements in the type is equal to the product of the cardinals of the types which form the index vector type xe vector index type list of type name index type list type name C type name 1 2 3 5 Structured type Elements of a structured type consist in contiguous elements called components which may be of different types Each com ponent is identified by a name The number of elements in the type is equal to the number of components in the declaration struct type xe struct component y component type name component name component name name 1 2 3 6 List type An element of a list type is a list which is defined as a finite sequence of elements of the same type The same item may appear several times in a list The following line declares a list type called bool list type bool list list nat of bool with capacity 10 An element of a list of type bool list has the boolean type The index type of bool list is the type be
92. st last_index suffix 1 2 9 16 Iterator Iterators are provided to express properties that must be verified by the net The general syntax of an iterator is the following iterator iteration scheme condition expression For more precisions on the notion of iteration scheme please refer to Section 1 2 8 7 An iterator considers all the tokens present in a place at the current state if the iteration domain is a place or all the values of a discrete type if the iteration domain is a type or all the items present in a container if the iteration domain is a container and computes a value A condition i e a boolean expression can be specified to limit the iteration to the values which satisfy the condition The evaluation of an iterator depends on its type Different types iterators are provided e Iterator forall checks that the expression is evaluated to true for all the possible iterations The expression provided must have type bool and so is the type of the resulting expression e Iterator exists checks that the expression is evaluated to true for at least one iteration No expression must be provided in the iterator The resulting expression has type bool e Iterators min and max compute respectively a minimal and a maximal value The expression inside the iterator can have any discrete type This type is also the type of the resulting expression If the set over which the variable iterates is empty the resulting express
93. t token component token component number Attributes attribute type attribute place attribute container attribute list attribute gt variable VU non empty expression list 1 expression C I non empty expression list expression empty non empty expression list variable 5 n expression C V expression z expression expression 7 gt expression 1 expression expression expression in expression empty non empty expression list 1 expression in expression expression or expression expression and expression expression expression x PE variable component name expression non empty expression list function name expression list type name expression gt sn condition true expression expression expression expression token gt component number variable name number hp type name type attribute place name place attribute expression expression list attribute first last card mult full empty size space first first index last last index U non empty expression list
94. t list small typedef struct TYPE_color items 5 of color with capacity 5 unsigned int length TYPE colorList typedef struct type smallSet set TYPE small items 5 of small with capacity 5 unsigned int length TYPE smallSet Sub types subtype tiny small 15 typedef TYPE small TYPE tiny typedef TYPE color TYPE rgColor define TYPE CONST rgColor red subtype rgColor color define TYPE ENUM CONST rgColor green 1 range red green define TYPE ENUM CONST rgColor blue 2 define TYPE ENUM CONST rgColor_ yellow 3 define TYPE ENUM CONST rgColor cyan 4 51 52 CHAPTER 4 INTERFACING HELENA WITH C CODE Table 4 2 Mapping Helena constants and functions to C Helena construct C construct Constants constant rgbColor BLUE 255 TYPE rgbColor CONSTANT BLUE Functions function isBlack rgbColor c bool return c r c g c b 0 TYPE bool FUNCTION isBlack TYPE rgbColor V2 e A structured type is mapped to a C struct type that has exactly the same structure e Acontainer type ct is mapped to a C struct type TYPE ct containing two elements the items of the list or set stored in an array items and stored in an integer component length the number of items in this array that are actually part of the container For instance the Helena expression red ex of type TYPE ct defined by gre
95. t N As soon as N states have been visited the search is stopped as soon as possible 2 1 5 Model options d SYMBOL NAME define SYMBOL NAME Define preprocessor symbol SYMBOL NAME a N capacity N The default capacity of places is set to N r run time checks Activate run time checks such as division by 0 expressions out of range capacity of places exceeded If this option is not activated and such an error occurs during the analysis Helena may either crash either produce wrong results L link OBJECT FILE Add file OBJECT FILE to the files linked by Helena when compiling the net Please consult Chapter 4 for further help on this option m p i parameter p i This gives value i an integer to net parameter p 2 1 6 Output o FILE NAME report file FILE NAME An XML report file is created by Helena once the search terminated It contains some informations such as the result of the search or some statistics Please report to Section 2 2 for further indications on this report i Dbrace Lype Specify the type of trace displayed e FULL The full trace is displayed e EVENTS Only the sequence of events the initial and the final faulty states are displayed Intermediary states are not displayed e STATE Only the faulty state reached is displayed No information on how this state can be reached is therefore available 34 CHAPTER 2 USING HELENA 2 2 The output report Once the search termina
96. t may differ in detail to address new problems or concerns Each version is given a distinguishing version number If the Program specifies a version number of this License which applies to it and any later version you have the option of following the terms and conditions either of that version or of any later version published by the Free Software Foundation If the Program does not specify a version number of this License you may choose any version ever published by the Free Software Foundation 70 10 11 12 APPENDIX B GNU GENERAL PUBLIC LICENSE If you wish to incorporate parts of the Program into other free programs whose distribution conditions are different write to the author to ask for permission For software which is copyrighted by the Free Software Foundation write to the Free Software Foundation we sometimes make exceptions for this Our decision will be guided by the two goals of preserving the free status of all derivatives of our free software and of promoting the sharing and reuse of software generally NO WARRANTY BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE THERE IS NO WARRANTY FOR THE PROGRAM TO THE EXTENT PERMITTED BY APPLICABLE LAW EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND OR OTHER PARTIES PROVIDE THE PROGRAM AS IS WITHOUT WARRANTY OF ANY KIND EITHER EXPRESSED OR IMPLIED INCLUDING BUT NOT LIMITED TO THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICU
97. t to be used in properties and simply consists of an expression state proposition xe proposition state proposition name expression state proposition name x name 1 3 Property specification language The property specification simply consists of a list of properties Helena currently supports two types of property state prop erties and temporal properties expressed in the linear time temporal logic LTL property specification property property state property temporal property 1 3 1 State properties State properties form the most basic type of property Helena can analyse A state property must hold in all the reachable states of the system A state property consists of the keyword reject followed by the description of the states that are rejected during the search When a state is rejected by Helena the search stops and Helena displays the trace 1 e the sequence of transition bindings which leads from the initial state to the rejected i e faulty state The keyword reject can be followed by 1 the keyword deadlock In this case Helena rejects states in which no transition is enabled 2 a state proposition name Helena rejects any state in which the proposition holds Accept clauses can be used to limit the rejection of states which do satisfy the reject predicate if a state verifies at least one of the accept clauses then it is considered that the state property holds at this state
98. ted Helena prints a report to the standard output This section details the structure of this report 2 2 1 Structure of the report This report is composed of four distinct parts the information report the search report the trace report and the statistics report 2 2 1 1 The information report This first report contain general informations such as the name of the net verified and the date of analysis 2 2 1 2 The search report This report contains various informations on the search such as the termination state of the search or the options enabled e g partial order The search can terminate in different ways the property is verified the property does not hold the search ran out of memory 2 2 1 3 The trace report When the property specified does not hold Helena reports in a trace report the faulty execution discovered In the case of state property this execution consists of a sequence of states so 5 such that so is the initial state and 5 is the faulty state reached by Helena For LTL properties this consists of an infinite execution violating the temporal property 2 2 1 4 The statistics report The statistics report is the last part of the report printed by Helena after the search This report simply consists of a set of statistics collected by Helena The statistics reported gives various informations on the analyzed net the size of the reachability graph or the memory consumption Let us point out that the type
99. tended to apply and the section as a whole is intended to apply in other circumstances It is not the purpose of this section to induce you to infringe any patents or other property right claims or to contest validity of any such claims this section has the sole purpose of protecting the integrity of the free software distribution system which is implemented by public license practices Many people have made generous contributions to the wide range of software distributed through that system in reliance on consistent application of that system it is up to the author donor to decide if he or she is willing to distribute software through any other system and a licensee cannot impose that choice This section is intended to make thoroughly clear what is believed to be a consequence of the rest of this License If the distribution and or use of the Program is restricted in certain countries either by patents or by copyrighted in terfaces the original copyright holder who places the Program under this License may add an explicit geographical distribution limitation excluding those countries so that distribution is permitted only in or among countries not thus excluded In such case this License incorporates the limitation as if written in the body of this License The Free Software Foundation may publish revised and or new versions of the General Public License from time to time Such new versions will be similar in spirit to the present version bu
100. tiplicities of these three tokens is 7 2 1 4 Container attributes Let c be a container i e an expression of which the type is a list type or a set type c size is the size of c i e the number of elements in this container This expression can have any numerical type c capacity is the value of the capacity of the type of c This expression can have any numerical type c space is the remaining space in container c i e the capacity of the type of c minus the number of elements in c This expression can have any numerical type c full is a boolean expression which value is true if the container is full 1 e the number of elements in it is equal to the capacity of the type of c or false otherwise c empty is a boolean expression which value is true if the container is empty i e it does not contain any element or false otherwise The following declarations illustrate the use of these attributes type int set set of int with capacity 10 constant int set sl empty constant int set s2 Il 5 12 5S5l constant int set s3 Il 2 4 8 16 32 64 128 256 5121 constant int il s2 size IF il eq constant int i2 sl capacity i2 10 constant int i3 s2 space 7 19 0 6 constant bool bl s3 full bl true constant bool b2 sl empty b2 true 1 2 NET SPECIFICATION LANGUAGE Table 1 1 Summary of the possible attributes Expression Valid if I
101. tween brackets i e nat Let us note that this type must be discrete Indeed we will see later that the elements in a list can be directly accessed via indexes For example let us consider a list 1 of type bool list The expression 1 0 will denote the first element of the list 1 1 the second one and so on The capacity of a list type is the maximal length of any list of this type The expression provided must be statically evaluable and strictly positive Here the capacity is 10 This means that a list of type bool list cannot contain more than 10 booleans list type w list type name 1 of type name with capacity expression 1 2 3 7 Set type Sets are similar to lists except that the same item may not appear several times in a set Sets are not indexed Therefore no index type may be provided As for list types a capacity must be specified settype x set of type name with capacity expression 1 2 3 8 Subtype Discrete types can be subtyped Each subtype has a parent which can also be a subtype and is defined by a constraint which limit the set of values which belong to the subtype A constraint simply consists of a range which must be statically evaluable and which bounds must belong to the parent of the subtype Here are some examples of subtypes definitions 1 2 NET SPECIFICATION LANGUAGE 11 type small range 0 255 subtype very_small small range 0 15 subtype
102. type was for example the type short the first element would naturally have index 32768 It is possible to assign a value to an element of a list at a specified index The syntax is the same as for vectors except that only one index can be specified If we consider the list 1 previously defined then the expression 1 2 10 has type int_list Its value is the list 1 in which the element at index 2 has been replaced by the constant 10 In other words 1 2 2 10 Il 2 10 4 51 An error is raised if an attempt is made to assign a value to an element at an index which does not exist e g 1 5 10 is an error Another possibility is to extract a slice i e a sub list from a list To do so it is necessary to provide the indexes of the first and the last elements desired The resulting slice consists of the sub list which contains all the elements of the original one from the first index to the last index As an example let us considered the list 1 previously defined Then 111 3 is equivalent to the list 11 1 1 2 11511 It is important to notice that in the resulting list the index of the first element will still be i e the first value of the index type nat and not 1 To be correct a slice must be such that both the first and the last index must be less than or equal to the index of the last element of the list If the index of the last element is less than the index of the first one the resulting list is th
103. us consider for instance the expression s b not s b where the type of s is the type t previously defined This expression has the same type of s i e t and has the same value of s except that its component b is replaced by the expression at the right of symbol To be correct such an expression must respect three rules 1 Expression s must have a structured type t 2 The replaced component i e before symbol must be a component of type t 3 The expression after symbol must have the same type as the the replaced component in the structured type declaration structure umo 74 non empty expression list structure component variable component name structure assignment expression component name expression 1 2 9 11 Vectors The handling of vectors is very similar to the handling of structures Three basic constructions allow to do this Firstly vectors can be constructed by placing the list of elements in the vector between characters and All the elements in the vector must have the same type The vector can be of any type which fulfills the two following conditions 1 The element type of the vector type must be the same as the type of the expressions in the vector expression 2 The number of elements of the vector type must be greater or equal to the length of the list The order of values in a vector is determined from left to right If the size of t
104. ve request of client d c transition balancer_route in balancer routing lt 1 c gt out balancer_idle incr l 11 gt server request lt c Il gt let server id Il least 1 description lb route request of client d to server 3d c transition balancer_receive_notification S 112 c 43 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 D I A tn D 44 CHAPTER 3 EXAMPLES in balancer_idle lt 1 gt server_notification lt s out server notification ack s balancer balancing lt decr l s gt description lb receive notification of server_ d s transition balancer_balance in balancer balancing lt 1 gt server_request lt c most 1 gt out balancer_idle lt decr incr l 11 ml gt server_request lt c Il gt let server id 1l least 1 server id ml most 1 guard not is balanced l description lb redirect request of client d from server d V to server 2d c ml 11 transition balancer_no_balance in balancer balancing lt 1 gt out balancer_idle 1 lt 1 guard is balanced 1 description lb no rebalance
105. very_small is equivalent to small without the values from 16 to 255 type color enum chestnut dark_blue green blue pink yellow subtype light_color color range green yellow subtype light_color contains values green blue pink and yellow subtype very_light_color light_color range pink yellow subtype very_light_color contains values pink and yellow The subtypes nat natural numbers short short numbers and ushort unsigned short numbers are predefined subtypes defined as follows subtype nat int range 0 int last subtype short int range 32768 32767 subtype ushort int range 0 65535 vvhere int last is the last value of type int see Section 1 2 9 15 subtype subtype name parent name constraint subtype name x type name parent name type name constraint xe range 1 2 4 Constants As in programming languages constants may be defined at the net level A constant is defined by using the keyword constant It must necessarily be assigned a value which must have the type of the constant constant ze constant type name constant name expression constant name x name 1 2 5 Places The state of a system modeled by a Petri net is given by the distribution or marking of items called tokens upon the places of the net In high level nets these tokens are typed This type is given by the domain of the place In the class of high
106. y Appendixes contain the syntax summary and the second version of the GNU general public license An index that references all the construction of the specification language of the tool can be found at the end of the document Contents 1 Helena specification language Li Lexical and syntame Conventions lt sooo Lu Roh Reno x Ro n A A dd 11 Lexraliobent x ot hak AA Feu AS bee S OX RR ere NU Ae o gs 11 2 Preprocessor directives aaan a ESE EAS Bah Azman Ge me TU hr 14 2550s 7 1 2 Weispeciicauentansuace dois eae add OH ERE Se eR ee OR x mea Ses LZ IR Mal INBE POTES neen AA ES Ee A EE ee E 123 Types and SUDIPPES ci A A OR ADU c Lee JEGHSIBDIS cr He eee dev US Bee eee AA a 12 E onec x GO o hee Ae PRA ER A paie de Rea RU baal So RUE E ed LAS TANSMONS 2 coppe Lu me ade ke ee D s ee ee ee ee ee des 1 27 PUNCUONS es bera REE EEE a e OS eS nom R 5 e LONE 0060100000 II Leo PEXDIBSSOBSC gt ici rd ee eh A Bee eae AA a L2 10 Are labels 12m a PEAR Re e RR A A L2 11 Sie proposihions uo 8 es eb So OR Re UR For SOR B B e ee de 908 PORTE he os 1 3 Property specification language o SO Rh A ER eR RS Be 13 1 IS oa m2 ae se 1 3 2 Temporal properties s c once ao eR wd e m S RUB Sr s 2 Using Helena z l a ns s R 5 sd Su BES BASE SHES SH dex ew dde s 211 General Opuons 2 4 5 6 ae ua si EUR RRA ee eee Re
107. y inhibitor arc Helena has to evaluate the labels of the input arcs of the transition its guard and finally has to pick all the possible acceptable values for its free variables defined in the pick section Hence three types of items have to be evaluated to bind all the variables of the transition and find enabled bindings tuples of input arcs the guard and free variables Each of these items define some variables i e bind them by giving them a value and use some variables that have to be defined so that the item can be evaluated The table below summarizes which variables are used defined by each kind of item Item Variables used Variables defined Tuple all variables appearing in the tuple all variables appearing in the tuple and not defined in it at the top level not in a sub expression Guard all variables appearing in the guard none Free variable all variables appearing in the definition of the variable the variable In the absence of inhibitor arcs a transition must fulfill the following requirement to be firable there must be an evaluation order items item such that for any i 1 n and any variable v used by itemi there is j 1 i 1 such that item defines variable v Otherwise the transition will not be evaluable This is for example the case with transitions t and u defined below transition t in p x f y y x 2 gt out q x transition u
108. ypes are mapped to the three following types typedef int TYPE_int typedef char TYPE_bool define TYPE__ENUM_CONST_bool__false define TYPE__ENUM_CONST_bool__true 1 typedef struct TYPE_int items 1000 unsigned int length TYPE_intList We first notice that each Helena type myType is mapped to a C type TYPE_myType For the boolean type TYPE_bool we notice that its constants false and true have been mapped to 0 and 1 The list type intList is mapped to a structured type TYPE_intList with two components e items is the content of the list stored in an array The size of this array is equal to the capacity of the list type intList 4 2 THE INTERFACE FILE 49 e length is the length of the list i e the number of integers in array items that are actually part of the list We are now able to write the three functions that are imported in our net specification Each function has been put in a separate file The content of these three files is depicted on Figure 4 1 For each imported function myFunc in the net declaration there must be a C function IMPORTED_FUNCTION_myFunc The return type and the parameter types of the C function and the function in the net declaration must match Otherwise a compilation error will occur when invoking Helena Now that we have written our imported functions we can analyze this net with Helena First we compile the C code of imported functions as follows gcc c initList c gcc c quickSort c

Helena 2.3 User's guide

Contents

Download Pdf Manuals

Related Search

Related Contents