Home

TECHNISCHE UNIVERSITEIT EINDHOVEN Department of

Contents

1. Fg t d gt 2 0 3 s v Y OS rule 21 For some p p o we have p v p v and t Og p t On p l o By induction and OS rules 1 2 3 4 5 we have Ja s d gt c p Fg p d gt ev gt s v Therefore by definition of Fr r p we have Jaws d gt x t Fg t d gt zv s v OS rule 24 For some X p we have t X and X p E and p v p rhs X By induction Jess e gt x t Fg q Ale gt pu gt definition of Fg X we have Jaws d gt x t Felt A d gt 2 4 gt s v t v Note that s v Thus by F C 4 Renaming operators All proofs related to the extension of Fg t with renaming operators are here It turns out that we need to assume that the solutions of a clause are not dependent on the name of the model variables i e v v E d iff V v V v E V d and v 0 c iff V v V o E V c This is a reasonable restriction on the clause formalism Theorem C 7 Well definedness The extended version of F t is well defined for substitutably guarded specifications Proof Take the weight function w t from theorem 4 2 In the new Fr t rules only Fg p is evaluated This decreases the number of operators as well as the number of possibly unguarded recursion 106 C 4 Renaming operators variables Therefore w p E lt w t E in each rule Theorem C 8 Form of Fr t
2. Ud Ne gt ev ild gt ev EeFrlpnale gt e v Felo U d e ex q q i d e v Fu p A e gt q q Fela U t p Oa pp Fr p else p p q pp Felp 8 Fr p K q dmev i p K q Fr q d gt ev Fu p i p p Fg p j CC II d gt e v 9 FelpD q U p p q d gt e Vv Fr p p p Fg p Ene ev i d ev eFz p eme v ce Fel d x Cijmp A da P C2imp gt C1 A ca H q i dy gt ey p Fg p da gt c2 q Fe q d gt c p i d gt c p Felp Ale gt ev Fz q 10 Fz plag E e d cq ld gt cq E Fpl Ale gt e v Fg p d gt ap ll q 1 d gt a p Fe p d gt aplqd 1i d gt aq Feal di Ada gt a p q i dy gt a1 p Fg p do gt a2 q Fg q A y a1 a2 a 11 Feun Ld d gt a p lg d gt a p Felp 12 Fz p q dd Ae Sed See Pen Ale ev E Feal U di Cijmp da Cojmp gt C1 eo H q di ep Fg p da gt c2 q Felq U e d gt c p 1 d gt cp Feun A e gt ev Fr 4 U Ke vd gt ed ildeed e Frlg Ale gt e v Fen L U di Adz gt a p q d gt a1 p Fg p A da gt az q Fg q A y a1 a2 a 13 Fr On p d gt d d p 1 d gt a p FE p ag A U i d2608u y i d gt op Fu p U d gt e6 v 1 d gt e Vv Fpp Il 14 Fg X Fg rhs
3. actcomm ropen sopen open rclose sclose close initial proc I encap halves X Y 2 This encapsulates the actions ropen sopen rclose sclose General restrictions Names of actions model variables and recursion variables must be unique They consist of a letter followed by zero or more letters or digits and may not be equal to any of the reserved words clause formalism act comm actcomm var def initial proc delta epsilon rename varrename Vm halves The clause formalism that is used may impose further restrictions on names of model variables and constants A clause predicate or a definition may be any string as long as all opening and closing square brackets are matched Comments and whitespace Comments start with 4 and stop at the end of the line Comments may not occur within clauses or definitions White space is a space tab newline or a comment Example HyPA model Table 5 7 gives an example of a model in the input file format 5 3 Clause formalisms In the course of the development of the simulator several clause formalisms are created After the prototypes we design clause formalism number 1 as a first attempt In order to satisfy modularity requirement 4 this is a self conceived language that is not solver dependent After this turns out to be cumbersome to implement and restrictive to the user the Mathematica specific mathematica clause formalism is designed However nume
4. yly amp ylz dx 6 re ylz e x zeqvyl z elc z x coa alylz xl ylz cld a 6 ao xiboy yla b O x y if y a b defined aoz boy 6 if y a b undefined ab xico y al dr yo j E yl c gt xe cb PIC U m al K ye yle z 18 2 2 Algebraic reasoning in HyPA Table 2 8 Axioms of HyPA part 2 On c c On a P y Ou x 9 On y 8 On e y LO y Ou x O On y On 0 du Lr gt y 0H 2 gt On y Ola x aifaeH y la ifagH true gt c d gt 10y m d gt u0d gt y false gt x d gt a or x dear d gt x d gt c Oz x dee 9 ded gt r x ded s d gt Or x d gt e d gt x0d gt zx x dvd gt u d gt xr gt y x d gt zuby imp DuC SE ag dee ly x d gt aly Og dz x d gt du 1 deld gt e Ad c deeld gt aor x d aO r d a Oy dAd gt a c 2 y if y a a defined d gt aorid gt a40y 6 if y a a undefined deeld err x Ld dC T 10 d gt c gt ald gt aoy x 0 d gt epald gt d py decCimp A d Hip gt al dr yo yl c gt zo i r d K yo ylc x Table 2 9 Recursive Specification Principle SEE S EE E guarded S X r S X Y 19 Chapter 2 HyPA semantics and axioms 20 Chapter 3 Requirements This chapter lists all requirements for the HyPA simulator First the requirements are summarized in the next section Then all requirements are listed including their motivation and current status Finally a table of requirements so
5. Perform transition Perform transition Perform transition PN oa y K d K N NN b i 4 Start IM L 2 2 0 NN N y H j 1 j ww N d i K 4 L p Close ne Undo i Possit Undo poor Undo K ae i d NS ze K X NC N 5 Close Load 5 1 2 3 Simulation The SimulationManager class controls the mode of simulation The visualization manager directs most user commands directly to the engine but not the retrieval of the set of first transitions Instead the simulation manager retrieves the first transitions solves them and eliminates transi tions without solutions An example of the communications involved is in figure 5 6 Random simulation is achieved through the creation of a thread figure 5 7 The thread commu nicates with the engine It repeatedly retrieves the set of first transitions picks one and solves and performs it Every so many seconds it communicates all state changes back to the visualization manager Having an extra thread implies that some form of synchronization is needed The simulation manager communicates with the engine and with the visualization manager Design decision 5 6 Synchronization The engine has all its public methods declared synchronized so that no two threads can access it at the same time The communication to the visualization manager is buffered and synchronized so that only the main thread manipulates visual controls 5 1 3 Interface We define t
6. ov p V v ove V 30 Theorem 4 9 Robust bisimulation is a congruence for model variable renaming Robust bisimulation is a congruence for model variable renaming Proof The OS rules for variable renaming are in the process tyft format as well Along the lines of theorem 4 8 we get that robust bisimulation is a congruence for model variable renaming as well 4 2 3 First transitions function To accommodate the new operators we extend the definition of Fg t Definition 4 10 Fp t extension We extend the definition of the first transitions function with 42 4 2 Additional HyPA operators 15 Felpalo d gt e v 1 d gt e v Fe p uU d gt A a p xe d gt a p Fe p U dee pa p 1 d gt ep Fr p 16 Fe ev p Vid gt eV dom e Y Fz p U V d gt a ev p 1 d gt a p Fr p U V d gt V c 0v p d gt ep Fz p In the proofs of the following theorems it turns out that we need to assume that the solu tions of a clause are not dependent on the name of the model variables ie v v E d iff V v V v E V d and v 0 c iff V v V o E V c This is a very reasonable restric tion on the clause formalism Again proofs of the theorems can be found in appendix C Theorem 4 10 Form of Fzg t The form of Fg t as shown in theorem 4 1 is left intact by the new rules Theorem 4 11 Well definedness The ext
7. t Let n Y N Redefine the first transitions function Fg t to F t by replacing rule 14 with 14 FR X if n X 0 then else FROM pps x Here n n X 1 n X means the mapping n with the value n X replaced by n X 1 Definition 4 9 max Nmax 18 a user supplied constant mapping that maps all recursion variables to the same constant This constant must be greater than 0 F t terminates take weight function w n t n o where o is the number of operators in t This weight function decreases with respect to the lexicographical order where ny X n iff Vxey no X m X The reason that we make n a mapping and not a single number is to maintain completeness of F r t for substitutably guarded models Because Nmar X gt 1 each recursion variable is allowed to be substituted for its right hand side at least once A value of 1 for nar X is sufficient for substitutably guarded models Suppose that t E is substitutably guarded and that a value of 1 is not sufficient Because of Fg t rules 7 and 9 FR X is only evaluated for unguarded occurrences of X Since a value of 1 is assumed to 39 Chapter 4 Analysis be insufficient F X needs to be called within a call to FE X This means that X occurs unguarded in its own equation This implies that no finite number of substitutions of X by its right hand side can make the equation guarded Now we have a contradiction the model is not substit
8. HyPA 6 7 is a relatively new process algebra that allows for the description of processes that have continuous as well as discrete behavior The goal of the language is the analysis of such hybrid systems see 6 section 1 3 Among the tools for such analysis a simulator is thought to be useful It provides the modeler with a first visual indication that the model indeed describes the desired process before more time consuming analysis tools are applied 1 2 Related work There already is a linearization tool for HyPA described in 18 It converts a large class of HyPA specifications to equivalent simpler specifications that use a subset of the HyPA operators This tool might provide a starting point for a simulator from the resulting form the possible first transitions are relatively easy to derive However in section 4 1 we explain why we do not take this approach Hybrid x 14 is another hybrid formalism developed at the TU e A simulator is being constructed simultaneously with ours There are other hybrid process simulators like cHARON 1 and HyVisual 9 cHARON is a hybrid process language that comes with a simulator and a visual editor HyVisual is a visual modeling language with a simulator For visualization of the values of model variables both simulators use the PtPlot Java library 13 that we used in our prototypes as well 1 3 Development process Since this is a relatively small project with only one programmer n
9. In each of the axioms x y z denote arbitrary terms The letters a a denote actions while c denote flow clauses and d d denote re initialization clauses One may not choose 6 when a is written in an axiom 2 2 3 Recursion principles When reasoning about recursion it is often useful to have a principle that claims that a solution of certain recursive specifications exists and is unique That a solution exists follows directly from the operational semantics of HyPA but it is not always clear that this particular solution is the only process satisfying the recursive equations Let us first define what we mean by solution Definition 2 9 Solution Let E be a recursive specification An interpretation S V T V of recursion variables as process terms is a solution of E denoted S E if for every recursive definition X p E we have S X amp S p where S p denotes the process term induced by application of S to the variables of p In particular S X is called a solution of X p E 16 2 2 Algebraic reasoning in HyPA The recursive specification principle RSP which is quite standard in process algebra states that so called guarded recursive specifications have at most one solution For HyPA guardedness of a recursive specification is defined as follows Definition 2 10 Guardedness An open process term p is guarded if all occurrences of process variables in p are in the scope of an action
10. The form of Fg t as shown in theorem 4 1 is left intact by the new rules Proof By construction Theorem C 9 Soundness termination Termination in the extended version of Fg t implies that t E can terminate To prove 1 da d gt ev Felt A d gt evy gt t v v Proof Extend the proof of theorem 4 3 with the following Rule 15 t palp d gt e v Fz p for some p By induction and OS rule 25 Rule 16 t oy p d V d d gt e v Fr p for some p d From d gt e v v we conclude Jy v v Hr d By the extra assumption v v E d By induction p v v By OS rule 28 t v v Theorem C 10 Soundness transitions All transitions in the extended version of Fg t can be performed by t E To prove Sas d gt 2 1 Fe t A d gt 2 0 gt s v gt tv gt v Proof Extend the proof of theorem 4 4 with the following Rule 15 t palp t pA p for some p p A We have two cases e Case 1 x A a d gt a p Fg p for some a By OS rules 2 and 5 we have that l A a v and v v E d Again by OS rules 2 and 5 d gt a v 0 e v By induction we have that p v p v By OS rule 26 we get t v gt t v e Case 2 x c d gt x p Fg p for some c By OS rules 5 and 3 we have that 0 for some c By induction and OS rule 27 we get t v t v Rule 16 t ov p d V d t ov p
11. g 981 x 10 2 f 70 x 102 BouncingBall speed gt 0 gt Up amp speed lt 0 gt Down Up altitude speed altitude t speed t A speed t 1 x g speed t 20 gt speed U gt Down Down altitude speed altitude t speed t A speed t 1 x g altitude t 20 gt speed altitude 0 A speed 1 x f x speed gt Up 79 Chapter 7 Cases Figure 7 3 Bouncing Ball simulation results 7 5 Simple test This model shows that the model variable renaming operator introduced in section 4 2 is useful The calculations for the X and Y directions are the same We introduce processes that only calculate values for the X direction We run that process in parallel with itself with variables renamed for the Y direction In figure 7 4 there are two plots The top one shows the speed in X and Y direction You can see that the speeds reverse direction on each bounce and that the speed decreases due to the friction The bottom one shows the position of the ball This shows that an X Y plot is a natural way to visualize some systems you can actually see the ball bouncing around the table The initial kink in the line starting from coordinates 0 0 is from the reinitialization at the beginning of the model The simulator had its initial variable values all set to 0 and then the reinitialization placed the ball on coordinates 5 2 Table 7 4 Billiards model A Vin
12. mx My VX VY X yl f 5 x 1077 stopspeed 1 x 107 Billiards xt 5 A maT 40 A Vx ERA S illiards mx my vx Vy X y y 2 A my 10 vy 3 MovePos omxemy vxervy xy MovePos x t 2 0 vx t 0 ln E PEPE OA ver Oo etl Oee VE vx gt 1 xstopspeed gt Still e vx x 0 vxt 2 vx gt MovePos MOERS OEVER po MDO AD P XE WO SR x t lt mx t A vx t gt 0 vx lt stopspeed gt Still Vx x MX A vxt vx gt MoveNeg Still mx vx x mx t 0 A vx t 0 x t 0 7 5 Simple test Table 7 5 shows a model that allows the user to freely simulate any behavior In each step the user has the choice between an action a flow one in which the variable may jump or successful termination The flow is not specific so the user will be asked for a predicate each time 81 Chapter 7 Cases Figure 7 4 Billiards simulation results Table 7 5 Simple test model A a Vin x I aole True e 10 82 7 6 Half wave rectifier 7 6 Half wave rectifier Figure 7 5 shows a half wave rectifier circuit taken from 17 It consists of a diode D two resistors with resistance Ro and Rij respectively a capacitor with capacity Co and a voltage source with voltage vo The source voltage is a sine wave with frequency f For each component in the circuit there is a process in the HyPA model For the passive com ponents
13. 3 2 Requirements 3 2 2 Clause formalisms The HyPA specification does not say much about the form of flow and reinitialization predicates We investigate what types of clauses occur in literature and base requirements on that 3 2 2 1 Clauses in literature In this section we investigate what clauses occur in examples in literature We use this knowledge to formulate requirements and in section 5 3 to design actual clause formalisms The following example clauses were taken from 18 6 and 14 Some clauses were simplified e pumping true lastgatepos g2 0 _gatepos mode opening gt gatepos Vyate mode closing gt gateposy Vgate e lastpressure lt Primit pumping pumping true e lastpressure lt Primit V lastgatepos ya 0 e Near r from V VvV 0Q 0s Qmin Z Qs lt Quas e Q 0 t URLS T e Vmin Vsafe lt VT lt Vas Vsafe Generalizing we encounter the following constructs in clauses e General Model variables constants and literal values are strings reals or booleans Pre defined functions and predicates are used e Reinitialization clauses Equalities Inequalities 4 lt lt gt gt Boolean operators V gt true and false e Flow clauses Equations Q t 0 Ordinary differential equations V t Qi t Qs t Predicates on the value of a model variabl
14. 7 sequential composition _ 8 disrupt gt _ and left disrupt _ gt _ 9 parallel composition left parallel composition _ and forced synchronization 10 a family of encapsulation operators On gc 4 Deadlock and the empty process The atomic process terms called deadlock and e called empty process are used to model 8 process that shows no behavior at all i e that has inadvertently stopped functioning and a successfully terminating process respectively Discrete actions The atomic discrete actions are used to model discrete computational behavior The set A of discrete actions is considered a parameter of the theory and can be instantiated at will by the user of our hybrid process algebra Chapter 2 HyPA semantics and axioms Flow clauses Flow clauses are used to model continuous physical behavior Traditionally in systems theory several different formalisms are used for the description of continuous behavior and often the modeling or analysis question determines which formalism is to be used Common to all approaches is that continuous behavior is described by some sort of predicate on the flow of values of model variables Vm through time Formally we write Y LJ ey Y x for the union of all model variable domains and Val Vm V for the set of variable valuations The set of all flows is F f T Val dom f 0 t for some t T Note that these functions al
15. Cd gt x t Felt Ald gt z v gt s v OS rule 16 For some p p q q 0 we have pv p v and q v q v and I o t p d and either t p q or t plg By induction Jg es di gt cp Felp di gt a v s 07 and Auer w d2 gt 9 8 Fg t dg gt c2 v u v By OS rules 3 and 5 we have v 0 t and Jy v vi di v1 0 E c1 v v2 E da va 0 E c2 and dom a IS 0 t for some t Now let v a 0 Since if 3 v 0 E c then 9 0 0 E c we have that v 0 E c and v c HF c Then by the definition of cjmp we have that v1 v cijmp and vo v ye H Cojmp Ww 105 Chapter C Proofs for Fr t The definition of d d gives us v v E di Cijmp and v v H da cojmp Combined and using OS rules 3 and 5 and the definition of we get d1 Cijmp da C2jmp gt 1 3 U 9 c1 co v This is what Fg p q and Fg p q return and therefore Jazo d gt x t Felt A d gt 2 0 gt s v OS rule 17 For some p p q 0 we have p v t v q v v l c t p Furthermore t plgort ql port p qort q p By theorem 4 5 we have 3 e gt e v Fg q e gt v v By OS rule 4 and the definition of we have v v e Induction Jap o d gt p p r Fg p d gt p v s v OS rule 5 gives 3 v v E dA
16. F 7 2 3 Zooming and scrolling You can zoom in on a portion of a plot by dragging your mouse across the area in a down right direction There may be a short delay before the zoomed area is visible because the simulator might have to ask Mathematica for more plot points Zooming out is done by dragging the mouse in the opposite up left direction During the drag you see two overlapping blue boxes The inner box represents the current view and the outer box represents the new view The difference between the old and new view is proportional to the difference between the boxes You can only zoom out until all the data in the plot is shown If you want to zoom out entirely you can also use button 15 You can scroll through a plot by dragging your mouse using the right mouse button You can drag in any direction and the plot will stick to your mouse pointer Note that the time axis ranges on all plots and on the action viewers are synchronized When you scroll through one plot all other plots will move as well This allows you to see the relationship between actions and the different model variables easily This goes for the X Y plots as well if the X T plots show a particular time range the X Y plots only show transitions from that time range F 7 2 4 Auto adjustment of plots It is not always handy to see all transitions at once The simulator can automatically adjust time ranges for you during simulation Drop down box 16 controls which tra
17. OS rule 4 gives d gt e v v Theorem 4 3 now gives p v v OS rule 5 gives us e gt q v gt s v Induction q v s v From p v vY and q v gt s v we get by OS rule 10 that t v t v Rule 8 t p q for some p q We have two cases e Case 1 p K q d gt 2 p Fg p for some p Induction p v p v By OS rule 12 t v t v e Case 2 d gt z t Fg q By induction and OS rule 14 t v gt t v Rule 9 t p gt q t p q d gt zv p Fg p for some p Induction p v p v By OS rule 12 t v gt t v Rule 10 t p q for some p q We have six cases e Case 1 p lg d gt x di Ciimp da Cojmp gt C1 e di gt a Fg p da gt co Fg q I co for some p q di do c1 c9 0 From OS rules 3 5 we know Iv v va t 0 va E di A vs v E Cljmp A v va E d A va v E C2jmp A v 0 E a A v a E c2 dom o 0 t Av a t s c Aes The definition of cjmp implies 102 C 3 Fg t is complete for substitutably guarded models that v3 0 E c1 v4 0 H c2 Now by OS rules 3 5 di gt c1 0 c1 0 t and da gt c2 0 c2 0 t Induction p v gt p v and q v q v By OS rule 16 we now get t v t v Case 2 t p d gt xv e sd gt c d gt cp Fg p e gt e V Felg for some p
18. or Jas d gt x t Fg q d gt x2 v gt s v This implies according to the definition of Fg p O q that Jas s d gt x t Felt A d gt 2 0 gt s v OS rule 9 For some p p q we have t p q t p q and p v gt p v By in duction we have Ja d gt v p Fg p d gt 2 0 gt s v Therefore we have by definition of Fg p O q that Jaws d gt x t Felt A d gt 2 v gt s v OS rule 10 For some p q we have t p q and p v v and q v t v By theo rem 4 5 we have Ja d gt e v Fg p d gt e v v By OS rule 4 we have 3y v v E d and thus v v F d By induction Je qr s e gt q i Fg qg e gt q v s v By OS rule 5 3yr v v H eA q v 5 gt ER Y Thus by definition of we have d e gt q v s v and by definition of Fg p O q we have Jas d gt z t Fg t A d gt z v s v OS rule 12 For some p p q p v p v t p K q andt p gt qort p P q By induction 24 d gt z p Fg p d gt z v s v By definition of Fg p K q and Fg p gt q we have Jaz d gt z t Felt A d gt 2 0 gt s v OS rule 14 For some p q we have t p K q and q v t v By induction Jas d gt x t Fg q A d gt z v gt s v and thus by definition of Fg p K q we have Aars
19. t v 5 t v Proof Proof by induction on w t E We suppose Jaws d gt 1 8 Fg t Md gt 2 0 gt s v For each case below we prove that t v t v Case w t E 0 t has no operators and no unguarded occurrences of recursion variables sotu e a c 6 Thus one of rules 1 through 4 of Fg has been applied to t and trivially the theorem holds Case w t E gt 0 We use case distinction on the rule of Fg used first Rules 1 through 4 cannot have been used Rule 5 t d gt p d x x d e gt p e gt p p Fr p t p for some d e p p p By OS rule 5 dy v v E d and v v H e and p v s v OS rule 5 read in the other direction now gives us e gt p v OS 5 gives t v t v s v Induction p ov gt p v and Rule 6 L p q d gt x t Fg p or d gt x t Fg q Induction p v gt t v or q v t v OS rule 7 gives t v t v Rule 7 t p q for some p q We have two cases e Case 1 p q d gt 2 p Fg p for some p Induction p v p v so OS rule 9 gives t v t v e Case 2 t q d gt x d e gt q e gt q q Fela d gt e V Fe p for some d e q q By OS rule 5 we have Jd v v d v v H eA q v 3 s v y From v v E d we conclude 3 v v H d
20. 1 package hypasim engine formati import java_cup runtime import java util import hypasim interface engine ui action code parser code Constructor that creates a HyPA_ASCII_scanner public HyPA_ASCII_parser java io Reader input j Parse method that returns a specification 128 G 2 JavaCUP input public Symbol parse throws java lang Exception Throw syntax error with line col info public void unrecovered_syntax_error Symbol symbol throws Exception try super unrecovered syntax error symbol catch Exception e throw new EHSParseException Syntax error on line symbol left column symbol right zu Terminals tokens returned by the scanner headers terminal CLAUSEFORMALISMHEADER ACTHEADER COMMHEADER VARHEADER terminal DEFHEADER PROCHEADER INITIALHEADER ACTCOMMHEADER separators terminal COMMA BAR EQUALS LABSTRACT RABSTRACT LPAREN RPAREN terminal LSQBRACKET LBRACE RBRACE RIGHTARROW LEFTRICHTARROW constants terminal DELTA EPSILON operators terminal CONCAT AND OR CJMP SAT REINITOP ALTERNATIVEOP SEQUENTIALOP terminal DISRUPTOP LDISRUPTOP PARALLELOP LPARALLELOP terminal ENCAP ACTIONRENAME VARRENAME special terminal String ID PREDICATE Non terminals non terminal spec non terminal String section non terminal String clauseformalism actions section var section non te
21. 14 c5 v q v By OS rule 5 we have that q co Trivially p v p v and p Rq Case 3 q d gt Cy l Co By OS rules 12 5 3 and the definitions of clause solutions we have v o 0 Hr true and Veev v x c 0 x and 9 0 0 Fy pred and q c K co This implies that v c Fy Co By OS rule 5 we get p v p v and by definition of R p Rq 110 Appendix E Screenshots This appendix contains screenshots of the various prototypes and simulator versions Figure E 1 shows the first prototype a dummy user interface with every visualization element in its own window There is a window containing the HyPA model to be simulated a list of all transitions that have been performed two X T plots showing the value of variables X and Y over time On the upper right there is the main window with all controls needed to run the simulation open files etcetera The list on the left of the main window is the list of current choices This window also contains a plot with all variables In the real version this plot could be used to select the time length of a flow clause to perform The second prototype is in figure E 2 The entire user interface is contained within one win dow X T plots are shown below each other and each X T plot displays the same time interval This makes the relations between the variables more clear Figure E 3 shows a working version of the HyPA simulator Simulation cont
22. 4 1 2 Simulating other classes of HyPA models 36 4153 Optimizations 3 5 2 Se da ad s 40 4 2 Additional HyPA operators eee 41 4 2 1 Action renaming RER RER NEN SR SN SEE e DE 41 4 2 2 Model variable renaMing e 42 4 2 3 First transitions function eeen 42 4 2 4 Model variable abstraction e e 43 5 Design 47 5 Architecturen ont mln Wa ace in di der ue Ld qe UR e deu e Cb a ae d 47 5l Rough division 2 213333 e808 A ae EE SPP S RA 47 5 1 2 User interfaces aa 54 id bee ee A eL ta ar aa 49 5 3 l terface sto n We DS A a a 52 Dl Engien oe ed AA HARES EEE e a eh a 60 932 Input le formal Must x ok anar ar Ae ethene tt Ne TR s Bae N a gh a fe 63 CONTENTS 5 3 Clause formalisms lt lt coa a cce cocoa maad u aa a aaa a aaa 67 5 3 1 Formalism number ame 69 5 3 2 Mathematica clause formalismo 69 5 3 3 Symbolic Mathematica clause formalism a 71 6 Implementation 73 6 1 Programming language n 73 6 2 Codingestyule natal AAA AA A ats MN ew a A 73 6 33 vDarsing nana am maa A A A A a hot A 73 6 4 Plottier wo ERA S RSS ue SS E er tied te ATG 73 7 Cases 75 t Steam bDoler ALi 2 5 355 A a A Se 75 1 27 T hermostatozt 44 de tein a foe eue ub lm nn lak hata dE a 78 f Bouncing balls 29326 NEE A 78 GAY BEA SEA edenda SD AAA A Ms E Did 78 9 DIMPLE RES oort zont DAR d ag a qaa 81 O Half wave rectifier sso a ua nde
23. Completeness transitions Every transition of t E is in the extended version of Fr t To prove tv 3 1 0 gt Sas s d gt x t Fg t A d gt 2 4 gt s u Proof Extend the proof of theorem 4 6 with the following OS rule 26 t pa p t palo I Ala v for some a v A p p and p v 4 p u By induction Jaz v d gt ap Fg p d gt 2 0 0 s v By the form of F t and OS rules 1 through 5 we have that x a By OS rules 2 and 5 we have that d gt A a v 40 0 s v Therefore by definition of Fy pa p we have Aar d gt x t Fg t Ald gt z v gt s v OS rule 27 t palp T pa p o for some a A p p c and p v gt p v By induction Jax d gt x p Fg p d gt 2 0 s v 5 Therefore by definition of Fg pa p we have Jaz d gt x t Fg t d gt 2 0 gt s v Y OS rule 29 t ov p t ov p I a V v for some a v V p pl and p v av p v By induction 34 4 d gt z p Fg p d gt 2 0 2 s v By the form of Fr t and OS rules 1 through 5 we have that x a By OS rules 2 5 and the extra assumption we have that V d gt a v Y s V v Therefore by definition of Fg ov p we have Jazo d gt x t F t A d gt 2 0 gt s v OS rule 30 t ov p t ov p I V o for some 0 V p p and p v p v By ind
24. Therefore we have w p E w p gt q E Rule 14 This is a substitution of X by rhs X so if w X E s 0 then w rhs X E s 1 0 for some o 99 Chapter C Proofs for Fg t Furthermore the precondition for Fg t is met in recursive applications t E in recursive ap plications Fp t is still substitutably guarded since substitutable guardedness only depends on E Theorem C 2 Form of Fr t By construction the value returned by Fg t is a set with elements of the form d gt a p deep dev Here p E is substitutably guarded since substitutable guardedness only depends on E C 2 Fg t is sound We prove that every transition that is in Fg t can be performed by the model Theorem C 3 Soundness termination Termination in Fr t implies that t E can terminate To prove da d gt ev E FE t A d gt ev gt t v v Proof Proof by induction on w t E We suppose that Ja d gt e v Fg t A d gt e v v and prove for each case that t v v Case w t E 0 t has no operators and no unguarded occurrences of recursion variables sotu e a c Thus one of rules 1 through 4 of Fg has been applied to t and trivially the theorem holds Case w t E gt 0 We use case distinction on the rule of Fg used first Rules 1 through 4 cannot have been used Rule 5 t d gt p d d ve e gt e v Fg p for some d e p From d gt e v v we conclu
25. a discrete action first and then behaves as a normal parallel composition with q or p cannot perform such an action and the process deadlocks The forced synchronization p q models how the first behavior either a discrete action or a part of a flow of p and q is synchronized after which they behave as in a normal parallel composition If synchronization is not possible then the forced synchronization deadlocks Chapter 2 HyPA semantics and axioms Encapsulation Encapsulation Oy p models that certain discrete actions from the set H C A are blocked during the execution of the process p This operator is often used in combination with the parallel composition to model that synchronization between discrete actions is enforced From the signature of HyPA terms can be constructed using variables from a given set of process variables Y with Vp N Vm as usual In this thesis the set of all such terms is denoted 7 V and these are referred to as terms or open terms Terms in which no process variables occur are called closed terms The set of all closed terms is denoted 7 Finally all the processes should be interpreted in the light of a set E of recursive definitions called recursive specification of the form X p where X is a process variable and p is a term We denote the set of all process variables that occur in the left hand side of a recursive definition from E by V V Vp and call these variables recursion variabl
26. a set of actions X denotes a recursion variable v v v denote valuations denotes a flow t denotes a point in time and I denotes an arbitrary transition label In table 2 1 the semantics of the atomic processes the flow clauses and the process re initializations is given Rule 1 captures our intuition that e is a process that only terminates Analogously the fact that there is no rule for 6 expresses that this is indeed a deadlocking process Rule 2 expresses that discrete actions display their own name and the valuation of the model 11 Chapter 2 HyPA semantics and axioms Table 2 1 Operational semantics of HyPA 5 0 Ec dom o 0 t 1 a nen testen bedient dies EET d gt pv m d pu 5 pv 2 Table 2 2 Operational semantics of HyPA alternative and sequential composition pv Y p v pv 6 7 BEET peent Ww a q p v gt pv l roy DY qv Y 8 p v pv 9 pOqv v pO qv gt p O qv pu Y qu gt q v pO qu gt q v 10 variables on the transition label but do not change this valuation Changes in the valuation can only be caused by flow clauses and re initialization clauses as defined by rules 3 to 5 The semantics of the other operators is defined in tables 2 2 2 3 2 4 and 2 5 Table 2 3 Operational semantics of HyPA disrupt EA nv gt PY qs pda eu us p gt qv gt p K qv 2
27. actions ITransitionChoiceObserver Choice of a transition ITimeChoiceObserver Choice of a time length of a flow transition IPerformObserver Performing of transitions IXAreaObserver Changing the position and size of X T plots IZoomScrollObserver Zooming and scrolling in X T plots Figure 5 4 Plot class hierarchy Background axes titles Zooming amp scrolling XYPlot XTPlot X Y data drawing NA X T data drawing A TimeChoiceXTPlot pr A A al Time choice bars 5 1 2 2 User input The VisualizationManager translates all user commands into corresponding commands for the engine or simulation manager and notifies the visualizations of any changes in the current state When necessary it pops up dialogs for the user to enter extra information Design decision 5 5 For each user command load specification perform this transition etc there is a method in 51 Chapter 5 Design VisualizationManager This keeps the visible controls and forms light weight all they need to do is call one method for each action that the user performs Typical user actions are shown in figure 5 5 The user loads a specification sets initial values and starts performing and undoing transitions Of course only performed transitions can be undone Finally the current specification is closed and or a new one is loaded Figure 5 5 User command statechart Set initial values ra z K x z g ex NS GE NS As S ve ISG p Load _
28. all performed flow transition lengths getInitialValues Returns the initial value for each model variable setInitialValues values Sets new initial values for the model variables getFirst Transitions Retrieves the transitions that the model can perform next solve transition Solves the clauses of a given transition performTransition transition solution Performs a given transition undo n Undoes the last n performed transitions closeSpecification Closes the current specification 55 Chapter 5 Design Figure 5 8 Engine facade Interface_engine_ui Engine engine RealEngine DummyEngine 5 1 3 2 Transitions The getFirstTransitions method of the Engine returns a set of Transition objects As de scribed in section 4 1 a transition returned by Fg t is a tuple p p Process p indicates the clauses that need to be solved and the type of transition It has one of the forms d gt a dee d gt e Process p called next process is the process term of the resulting state p v In case of termi nation the resulting state is denoted by v In our application the Transition object is more than just that tuple Firstly we frequently have sets of multiple tuples p p p p with the same process p As an optimization we represent these tuples by a single Transition object that contains process p with a set of processes L o Ha Secondly a place is needed to st
29. d e c By OS rule 5 d v v e v v E d ev e v Thus 3v v v E e Theorem 4 3 gives q v v OS rule 5 and induction gives p v p v and OS rule 17 gives t v gt t v e Case 3 analogous to case 2 Case 4 t p q x a d gt a p Fg p for some p a OS rules 5 and 2 yield a v for some v Induction p v p v OS rule 18 gives t v t v e Case 5 analogous to case 4 e Case 6 t p q d gt x di da gt a dy gt ay p Fg p dy gt ard Fg q y a1 a2 a for some p q d1 do a a1 a2 By OS rules 2 and 5 v v di A v v da Thus by OS rule 2 and 5 di gt a1 v e v and dz gt a3 20 e v Induction p v 11 p v and qv 42 q v Now OS rule 19 gives t v gt t v Rule 11 t p q for some p q This proof is similar to Rule 10 case 4 Rule 12 t p q for some p q This proof is similar to Rule 10 cases 1 2 3 and 6 Rule 13 t Og p for some H p We have two cases e Case 1 t On p x a d gt a p Fr p a d H for some p a Induction and OS rules 2 and 5 give p v p v and I a v OS rule 20 gives t v t v e Case 2 t Og p x c d gt c p Fg p for some p c Induction and OS rules 3 and 5 give p v p v and I o for some OS rule 21 gives t v t v Rule 14 t X d gt z t Fg
30. for any p Definition 4 7 First transitions of all recursion variables Let m be a first transitions mapping Now define the function IF MM M as follows F m X gt m X U Fg rhs X X V Now we would like to prove that F has a fixpoint and that that fixpoint is reached This can be done by proving that F is continuous Then the theorem of Tarski Knaster 4 15 states that it has a unique least fixpoint given by LisoF 0 For continuity we need to prove that F is monotonic and that P M is finite For finiteness of P M we need restrictions on the HyPA models Finiteness of the first transitions mapping reeks of bounded non determinism definition 2 11 For example the not bounded non deterministic process X where X X a X can reach an infinite number of states by performing one a transition c 0 X eco X ox Bounded non determinism helps because it limits the possible number of states that can be reached by a transition However this does not limit the number of possible transitions from a given state In this respect we are helped by existing restrictions of the simulator Firstly the sets A and V are finite because the simulator has no syntax to specify infinite sets Furthermore the first transitions function abstracts from model variable valuations and flows This implies that P M is finite with respect to robust bisimilation for bounded non deterministic processes 38 4 1 First tra
31. if e for all z y X such that x Ry we find x implies y v e for all z y X such that x Ry we find y v implies x v e for all z 2 y X such that z Ry and AU X we find zx A 2 implies there exists y such that y 4 y and a Ry e for all z y y X such that z Ry and l AUD we find y 4 y implies there exists x such that x 2 2 and a Ry Two states z y X are bisimilar notation x y if there exists a bisimulation relation that relates x and y In lifting this notion of equivalence on hybrid transition systems to process terms and hence abstracting from valuations we have to be careful It is assumed that the model variables that are shared by the process terms to be related represent the same entity Therefore both process terms are only compared with respect to the same arbitrary initial valuation of the model variables Definition 2 5 Bisimilarity Two process terms p q 7 V are bisimilar denoted p q if there exists a bisimulation relation RC 1 V x Val x T z x Val such that p v R q v for all valuations v Val As it turns out this notion of equivalence leads to problems in combination with the parallel composition of processes This is due to a possible sharing of variables between processes As an 14 2 2 Algebraic reasoning in HyPA example one might study the following discrete systems X sa Felle le rl Y al z
32. lengthy calculations in Mathematica The random simulation stops in the following cases e Deadlock or termination e No solutions or only under specific solutions found e User abort using button 7 Alternatively you can start random simulation with button 10 You are first presented with a dialog that allows you to specify a stop criterium In addition to the cases above random sim ulation will also stop on reaching the stop criterium During random simulation the user interface becomes a bit sluggish However all non grayed elements can be manipulated with some patience F 7 Visualizations Model behavior is visualized with the action viewer X T plots and X Y plots 119 Chapter F User manual Figure F 5 Action viewer 10 00 11 00 12 00 action ERMINATION laction Figure F 6 X T plot Value Variables mx my vx vy X y versus time Time now F 7 1 Action viewer The action viewer figure F 5 is a fixed element you cannot remove or add action viewers It remains at the top of the screen It shows actions against a time line Actions are in red The range of the time line is kept in sync with the time axis of any X T plots That means that zooming scrolling in the X T plots described below also affects the action viewer When there are too many actions to fit next to each other actions are shown below each other In case of successful termination
33. maximum possible time length This maximum time length is limited by a user specified time limit Motivation See requirement 41 below Status Fulfilled 26 3 2 Requirements ID 12 Priority 4 Description Random simulation is possible i e all choices are made by the simulator The visualizations are updated continuously The simulation is stopped on deadlock termination and on user command Motivation Status Fulfilled ID 44 Priority 4 Description The stop criterium for random simulation can be the occurrence of a given action Motivation Status Fulfilled The user can select one or more actions that stop the random simulation ID 45 Priority 12 Description The stop criterium for random simulation can be a predicate on the model variables Motivation Status Not implemented yet ID 41 Priority 13 Description The user can indicate that the maximum possible time interval is chosen for every flow transition in random simulation mode Motivation In many models the most interesting trace is one in which all flows run for their maximum time length Status Fulfilled ID 13 Priority 8 Description The user can undo steps whenever the simulation is stopped Motivation Status Fulfilled ID 28 Priority 9 Desc
34. models which variables are allowed to change Note that this is precisely opposite to flow clauses where V denotes those variables that do not change The set of all re initialization clauses is denoted D The set D is closed under conjunction A disjunction V and concatenation of re initialization clauses Also there is a satisfiability operator d on clauses d D which does not re initialize the values of a model variable but only executes the re initialized process if d can be satisfied in some way And finally there is a re initialization clause Cjmp derived from a flow clause c C which executes the same discontinuities that are allowed initially by the flow clause These last two operators turn out to be especially useful when calculating with process terms Using the assumption that there are re initialization predicates false and true we find the process re initialization false gt p executing no behavior since there is no re initialization satisfying 8 2 1 Syntax false the process re initialization true gt p executing exactly the behavior of p since none of the variables is allowed to change and the process re initialization Vl true gt p executing p after an arbitrary re initialization Alternative and sequential composition The alternative composition p q models a non deterministic choice between the processes p and q The sequential composition p q models a sequential execu
35. not likely to be found only in the case where x is exactly zero 70 5 3 Clause formalisms 5 3 3 Symbolic Mathematica clause formalism The numerical mathematica formalism has its problems e Constructions like V z t 2 1 z t lt 3 gt 7 3 gt a pose a problem since the exact value 3 is probably never reached due to calculation errors This leads to dead locks in the simulation where there would not be any in analysis e Sometimes the Mathematica NMinimize function returns an answer from which we cannot deduct wether the inequalities hold on the entire domain or not at all This happens for example when o t x 0 e The accuracy and precision of the calculation cannot really be determined by the user Therefore we introduce a new symbolicmma clause formalism that solves its clauses symbol ically Identifiers Variables constants and functions may have any name that Mathematica allows except for t and lt var gt lt suf gt lt n gt Here var is a variable name suf is P or N and lt n gt is a number The name t is used as a independent time variable for the differential equations The other type of disallowed identifier is used for temporary variable names during the solving process Using lowercase letters ensures that a name does not coincide with an existing Mathematica symbol Definitions In each det L 1 section mathematica commands may be listed that are executed prior t
36. of the minimum and maximum possible time length if such a minimum or maximum exists 21 1 Fulfilled It is clear at which time the discrete actions take place 50 2 Fulfilled In a transition choice all transitions are displayed Double clicking a transition chooses that transition and performs it 52 T Fulfilled The jumps in model variable values are visualized when an action transition is chosen but not yet performed 27 17 Fulfilled A legend can be shown in which the color for each model variable name is shown 22 17 Fulfilled The relation between two model variables can be visualized in an X Y plot 7 20 Not implemented The current locations of the simulation of parallel processes is visible in the original model text Deleted requirements The requirements below were deleted Despite their initial priorities of 18 and 19 their importance was deemed so low that it became clear that they would never be implemented ID Prio Status Description 26 18 Deleted The sequence of performed action transitions can be visu alized in a message sequence chart The user can indicate which action belongs to which process in the chart 25 19 Deleted The structure of the model can be visualized in a cir cle square line diagram analogous to diagrams of x mod els 3 2 4 Simulation The requirements presented here define different modes of simulation We have
37. rhs X By induction rhs X v t v By OS rule 24 we get t v t v C 3 Fg t is complete for substitutably guarded models We prove that everything that a model can do is in Fr t Theorem C 5 Completeness termination Termination of t E is in Fg t To prove bu gt da d gt e V Felt do e v v Proof Proof by induction on the length of the derivation of t v v We make no distinction between base and step cases We use case distinction on the OS rule applied in the last step in the deriva tion This can only be one of OS rules 1 4 6 8 11 13 15 22 23 OS rule 1 e and the definition of Fg c combined with axiom 9 1 implies Ja d gt e Y Fg t A d gt e v v 103 Chapter C Proofs for Fg t OS rule 4 t d gt p for some d p and 3 v v E d and p v v By induction 4 e gt v Fg p A e gt e v v By OS rule 4 this implies that Ayr v v E e and e v v Therefore v v E d e By OS rule 1 4 we have d e gt e v v By definition of Fg d gt p we now have Ja d gt e v Felt d gt e v v OS rule 6 We have for some p q that t p O q and either p v v or q v v By induc tion Ja d gt e v Felp A d gt e v v or dal d gt e v Fela A d gt e v v Thus by definition of Fg p q we have Ja d gt e v Fg t A d gt e v v OS rule 8 t p0 q p v
38. stage the required HyPAElement tree is created The HE1Element subclasses are listed in table 5 4 Table 5 4 HE1Element subclasses HEI1 Action An action or recursion variable HElActionRename Action renaming operator HE1 Atomic 6 or HE1Binary Any binary operator HE1Clause Any clause HElEncapsulation dv HE1Unary or Gimp HE1VarRename Model variable renaming 5 1 4 3 First transitions As stated before the first transitions function is distributed over the HyPAElement object tree Each HyPA element has a method getFirstTransitions that implements its own rule of the first transitions function Design decision 5 18 First transitions set To store the possible transitions a class FirstTransitionsSet is created It stores the differ ent types of first transitions termination action transition flow transition separately so that transitions of a type can be easily retrieved and enumerated 5 1 4 4 Clause formalism Design decision 5 19 Clause formalism Facade The ClauseFormalism class is a Fagade just like Engine For each different clause formalism there is a subclass The most important methods of the ClauseFormalism class are in table 5 5 The main purpose of the ClauseFormalism is to solve clauses The solve method does this It takes a Transition object and adds its solutions to it Each subclass overrides this method The getClauseFormalism method is static Given the name of a formalism it returns
39. the engine part and an interface engine ui package in between The latter package contains all classes for communi cating between the former two As a general rule classes in the ui package only know about the top two packages and classes in the engine package only know about the bottom two packages This is useful as a protection mechanism the user interface classes cannot reference anything inside the engine and vice versa so the division is enforced by the compiler Figure 5 2 Rough package division interface engine ui 5 1 2 User interface The user interface part has the following tasks e Receiving user input Enabling and disabling the controls for user input Visualization of the current state Synchronizing the position zooming and scrolling of the visualizations e Initiating different modes of simulation manual or random Design decision 5 3 UI division We divide the user interface into figure 5 3 1 Visible controls for input and visualization these include forms buttons plots etc 49 Chapter 5 Design 2 A VisualizationManager class that coordinates the visible controls 3 A SimulationManager class that controls the mode of simulation It controls when first transitions are calculated which of them are solved and it has a thread for random simula tion Figure 5 3 User interface static structure overview Visualization j o Subject Observer o VisualizationManager Observer S
40. this equational reasoning is also possible in HyPA We start out by defining a notion of bisimilarity on process terms reflecting equivalence of the underlying hybrid transition systems Then we study properties of this equivalence and capture those properties in a set of derivation rules and a set of axioms on the algebra of process terms Together with a principle for guarded recursion this forms a proof system in which every derived equality on process terms represents equality of the underlying hybrid transition systems In other words process terms that are derivably equal describe transition systems in the same equivalence class and hence describe the same process In the first part of this section we define the notion of robust bisimilarity In the second part we give a formal axiomatization of this notion and we treat the intuition behind the axioms and the insights they provide us with In the third part we discuss a specification principle that is used for reasoning about recursion 2 2 1 Robust bisimilarity of processes The hybrid transition systems that are used to give a semantics of HyPA contain an additional termination structure Therefore we start out by adapting the notion of bisimilarity on hybrid transition systems as follows Definition 2 4 Bisimilarity on hybrid transition systems Given a hybrid transition system X A 3 5 v see 6 definition 1 and 2 a relation RCX x X isa bisimulation relation
41. v q v v for some p q By induction Ja d gt V Fg p A d gt U V and delle gt ev Fg q e gt e v v By definition of Fg p q we have d Ae gt ev Fz t From d gt e v v and e gt e v v we know Ay v v E d v v Ke Therefore v v E d Ae and thus d Ae gt e v v OS rule 11 For some p p q p v v and t p gt qor t p gt q By induction Y Fg p d gt e v v By definition of Fg p gt q and Fg p gt q we have e v Felt d gt e v v OS rule 13 For some p q we have t p K q and q v v By induction Ja d gt e Fg q d gt e v v Thus by the definition of Fg p K q we have Ja d gt e v Fg t A d gt v v OS rule 15 For some p q we have p v v and q v v and either t p q or t p q This proof is analogous to the one for OS rule 8 OS rule 22 For some p we have t Og p and p v v By induction Ja d gt e v Fg p d gt e v v By definition of Fg Og p we have Ja d gt v Fg t d gt e v v OS rule 23 For some X p we have t X and X p E and p v v Note that p rhs X By induction Ja d gt e v Fg p d gt e v v and by definition of Fg X we have lld e V Felt Ald e v v 104 C 3 Fg t is complete for substitutably guarded models Theorem C 6 Completeness transitions Every transition of t E is
42. y y gt x as well as bidirectional ar rows x y may be used 65 Chapter 5 Design Table 5 6 HyPA to ASCII translation Description HyPA construct ASCII construct Deadlock delta Empty process epsilon Sequential composition Disrupt Left disrupt gt L gt Reinitialization gt gt gt Parallel composition E Left parallel composition IL IL Forced synchronization Alternative composition Encapsulation Flow clause Flow and Reinitialization clause Reinitialization and Reinitialization or Reinitialization concatenation Reinitialization satisfiable Cjmp Action renaming Model variable renaming dra het p Lu v w Lu v w gt lt gt Lu v w predicate predicate predicate P a b bc p z y yz D mp encap a b c p u v w predicate A u v w predicate A Y u v w predicate jmp rename a gt b b gt c p varrename x lt gt y p or varrename x gt y y gt x p 66 5 3 Clause formalisms Abbreviations Vm and halves A modeler often needs all model variables in the jump set of a clause The abbreviation Vm may be used for this purpose Example proc X Vm speed t 1 True Usually all actions that make up the halves of a communication are encapsulated by the Oy operator This may be specified by the abbreviation halves as shown here
43. your JavaCUP installation Do the same for the mathematica library but enter the path to JLink jar supplied with Mathematica 5 1 in the AddOns JLink directory Now you are ready to build the project You can build Java class files using Project Re build project hypasim jpx If you want to build Windows or Linux executables right click the native executable node in the project pane on the left named hypasim and choose Rebuild Detailed implementation documentation can be generated by right clicking the Standard Doclet node in the project pane and choosing Rebuild This generates JavaDoc HTML documentation 123 Chapter F User manual 124 Appendix G Input file format grammar For communication with future HyPA tools it is convenient to have a precise description of the input file format This appendix gives the grammars we used in combinations with the JFlex and JavaCUP tools to create a lexical scanner and a parser G 1 JFlex input The following is the input we fed JFlex to create a lexical scanner See the JFlex manual for details Input file for the JFlex lexical scanner generator Scanner definition for the HyPASim input file format number 1 package hypasim engine formati import hypasim interface engine ui import java util import java cup runtime Ah class HyPA_ASCII_scanner unicode cupsym HyPA ASCII sym cup Aline column fapiprivate switch Ayyle
44. z x if Var z AV 0 VA6 Vlzlly N Vlzly l if Var y NV VAT d gt V x RS V d gt z if Var d NV 0 VAS vla N w z if w g Var x VA9 Axioms VA1 VA2 VA3 and VA4 all express distribution of the abstraction operator over other operators Together they describe how abstraction can be distributed over closed linear terms Axiom VA5 describes how two abstractions can be merged Axiom VA6 states that ab stracting from variables that do not occur freely in the abstracted term has no influence Both of these axioms are useful for introducing abstractions or for eliminating them Axioms VA7 and VA8 expresses that a parallel term or re initialization clause can be pulled into the abstraction as long as the abstracted variables do not occur freely in that term or clause These axioms appeal to the same intuition as axiom VA6 However they cannot simply be derived from VA6 because abstraction does not distribute over parallel composition or re initialization in general Axiom VA9 states that abstracted variables can be renamed a conversion Note that in this axiom v and w denote single variables not sets of variables The expression z denotes the substitution of w for all free occurrences of v in the process term z 4 2 4 2 Simulator support for abstraction As noted in the section about model variable renaming all valuations have domain Vm Therefore there mu
45. 00 15 00 20 00 25 00 30 00 35 00 Ra ting D E ads ose lepen TT Chapter 7 Cases 7 2 Thermostat The thermostat table 7 2 taken from 5 is a small example to show that our plots can display curves nicely There is a heater that is supposed to keep the temperature in a room between two limits To do so it switches on and off upon reaching temperatures Tmin and Tmax respectively Two constants K and h influence the rate at which warmth leaks from the room and the amount of warmth generated by the heater The results are in figure 7 2 although this figure is a bit blurred Zooming in works fine and leaves the curves intact Table 7 2 Thermostat model A off on Vin T K 8x 1071 Ii 50 D 103 Tina 30 Thermostat ThermostatOn ThermostatOff ThermostatOff T T t KxT t T t gt Tmin gt T Tin gt on ThermostatOn ThermostatOn T T t Kx h T 0 T t lt Tmax 0 x gt off ThermostatOff 7 3 Bouncing ball The Bouncing Ball example from 5 is a nice model because it has very small time steps The model is in table 7 3 and the simulation results in figure 7 3 There is a ball that is dropped from a certain height The top plot represents the altitude of the ball and the bottom plot shows the speed Each time the ball hits the ground it loses some of its energy according to a factor L However the model is such that the ball never stops bouncing the
46. 1 clock t lt clockPeriod clock clockPeriod gt does not work the value of clockPeriod is probably never reached due to the errors introduced by numeric calculation This means that while the model does not have a deadlock it does during numeric simulation Therefore one has to adapt one s model to numeric calculation by eliminating equalities 75 Chapter 7 Cases Table 7 1 Steam boiler model A close nothing open rclose ropen sclose sopen y sclose rclose close y sopen ropen open Vin clock inflow steam water steamOut 1 inflowMax 2 clockPeriod 2 waterSafeMin 5 waterSafeMax 10 Boiler Orclose ropen sclose sopen Water Heater ValveOpen ValveClosed Controller Controller clock clock 0 gt clock clock t 1 clock t lt clockPeriod clock clockPeriod gt water gt waterSafeMax gt sclose Controller waterSafeMin lt water lt waterSafeMax gt nothing Controller water lt waterSafeMin gt sopen Controller Heater steam t steamOut inflow t inflowMax rclose ValveClosed ropen ValveOpen ValveClosed inflow t 20 rclose ValveClosed amp ropen ValveOpen ValveOpen Water water water t inflow t steam t 76 7 1 Steam boiler Figure 7 1 Boiler simulation results 0 5 000 10
47. A LAS ded dos 83 8 Conclusions 89 Bibliography 92 A Mathematical definitions 95 B Input restrictions 97 C Proofs for Fr t 99 C 1 F t is well defined for substitutably guarded models 99 0 2 Fg igsound tn amen ee ae Sa eh See CEA RRR Ee ee EE 100 C 3 F t is complete for substitutably guarded modes 103 CA Renaming operators 5 23 aba ege en an ai aen A dede de en N N R er en 106 D Rewriting flows 109 E Screenshots 111 F User manual 115 BET Installation x due eI See we dk d ee doe os dino Oh Old sita 115 B 2 IIE A uum me ust m mes T xou i dedere Qe eite e te edem dads 115 F3 UserdnterfACe uu lua a aa sed 115 FA Loading a HyPA model s 118 F 5 Step wisesimulation ee 118 BBL Solving transitions a 8 24 44 a a la RR hee amp AA AS 118 F 5 2 Choosing a solution ees 119 BG Random simulations cad e A es R r Rd en 119 FT VASUANIZALIONS ahy oss ih arras ot E Ei iot Tdi eus d dte puts 119 FILT FACTOR viewer r sos sneed IS wo qbus qa a MI ines da cb pedcs de 120 Br 2 AAA e oett A Teste ead atic ra M ah oe S 120 F8 Settings 25e RR oee eR RU EUR sl OA dee eee Hee aa 122 E92 Building 242 5 dr EE Se ood tec tie ie eid e f B a ti ue u 123 G Input file format grammar 125 Gal JElexnput oo 2 6 8 4 2 9 2 detains a ebbe oda 125 G Java UE input vw Pee RR ane Ba AE meren Re e MLB ed x des 128 Chapter 1 Introduction 1 1 Motivation and background
48. BAR ID s2 EQUALS ID s3 130 G 2 JavaCUP input var_list var var list var var list COMMA var var_section VARHEADER var_list 3 id_list ID s id list 1 ID s id list l1 COMMA ID s rename list ID i1 RIGHTARROW ID i2 rename list 1 COMMA ID i1 RIGHTARROW ID i2 ID ii LEFTRIGHTARROW ID i2 rename list 1 COMMA ID i1 LEFTRIGHTARROW ID i2 proc PROCHEADER ID var EQUALS proc_expr p INITIALHEADER PROCHEADER ID var EQUALS proc expr p 3 proc_expr ID id DELTA EPSILON LABSTRACT id list 1 BAR proc expr ci RABSTRACT LSQBRACKET id list l BAR PREDICATE pred LSQBRACKET BAR PREDICATE pred LSQBRACKET PREDICATE pred proc expr ci AND proc_expr c2 proc_expr c1 OR proc expr c2 proc expr ci CONCAT proc expr c2 proc expr d SAT CJMP LPAREN proc expr c RPAREN proc_expr c REINITOP proc expr p proc_expr p ALTERNATIVEOP proc expr q proc_expr p SEQUENTIALOP proc expr q proc_expr p DISRUPTOP proc expr q proc_expr p LDISRUPTOP proc_expr q p PARALLELOP proc expr q proc_expr p LPARALLELOP proc expr q proc_expr p BAR proc expr q ENCAP LPAREN LBRACE id list 1 RBRACE COMMA proc expr p RPAREN ACTIONRENAME LPAREN LBRACE rename list 1 RBRACE COMMA proc expr p RPAREN VARRENAME LPAREN LBRACE rename list 1 RBRACE COMMA proc expr p RPAREN LPAREN proc expr p RPAREN proc_expr 131
49. Pennsylvania Department of Computer and Information Science 2000 URL http www cis upenn edu mobies charon 2 J C M Baeten and W P Weijland Process Algebra Press Syndicate of the University of Cambridge 1990 ISBN 0521400430 3 Kent Beck Extreme Programming Explained Embrace Change Addison Wesley Professional 1999 ISBN 0201616416 4 Roel Bloo Herman Geuvers and Jozef Hooman Syllabus of the course Computational Models 2R070 Technische Universiteit Eindhoven 2000 5 Ed Brinksma Tomas Krilavicius and Yaroslav S Usenko Behavioural hybrid process calculus draft Technical report University of Twente 2005 6 P J L Cuijpers Hybrid Process Algebra PhD thesis Technische Universiteit Eindhoven 2004 7 P J L Cuijpers and M A Reniers Hybrid process algebra Journal of Logic and Algebraic Programming 62 2 191 245 February 1 2005 8 Erich Gamma Richard Helm and Ralph Johnson Design patterns elements of reusable object oriented software Addison Wesley 1995 ISBN 0201633612 9 Hyvisual URL http www ptolemy eecs berkely edu ptolemyII hyvisual2 2 index htm 10 Erwin Kreyszig Advanced Engineering Mathematics John Wiley and Sons 6th edition edition 1998 ISBN 0 471 85824 2 11 Mohammad Reza Mousavi Michel Reniers and Jan Friso Groote Congruence for SOS with data In Proceedings of Nineteenth Annual IEEE Symposium on Logic in Computer Science LICS 04 pages 302 313 Turku F
50. TECHNISCHE UNIVERSITEIT EINDHOVEN Department of Mathematics and Computer Science MASTER S THESIS Simulation of Hybrid Processes by R A Schouten Supervisors dr ir M A Reniers dr ir P J L Cuijpers Eindhoven August 2005 Master s Thesis for the course Technische Informatica 5 jarig TI5 R A Schouten ID number 456927 Contents 1 Introduction 5 1 1 Motivation and background e 5 1 2 Related work 224 bid da Aa 5 1 3 Development process 5 1 4 Structure of this thesis eee 6 2 HyPA semantics and axioms 7 2 1 AS WAKES Soe ee laisse AN 7 241 1 Formal semantics 2444 mams ded 79 Se He A A33 10 2 2 Algebraic reasoning in HyPA eeen 14 2 2 1 Robust bisimilarity of processes 1 a 14 22 2 Axiomatizatiow a 4 a ew eae A PREP ELS 15 2 23 Recursion principles ee 16 3 Requirements 21 3l OVERVIEW Jur AOR A A bec Be o EE AA te a E a 21 3 24 Requirements dt SR a Ae EN See ye EID ee Be EIE E ie Ar Bl 21 3 21 Ay PA PUT cc oa ee A eae e ee RR 21 3 22 Ola se formalisms zeiss A PUDE hx wee e Ib edd 23 3 20 Visualization ut s S ue doo Baeke SS S Ve d Z A 25 3 24 Simulation mierni A i A A RSEN NNUS US SR ES 25 3 20 Modularity 2224 2 sep AAA XY Y qe o E SD 29 3 3 Requirements sorted by priority en 31 4 Analysis 33 Ad SHirsttransitionsy wus vs tod mS Eee SC SI Aa de rus 33 4 1 1 First transitions function 0 0 00000 eee ee 34
51. X 35 Chapter 4 Analysis Fg t has the following properties The proofs for these theorems are given in appendix C Theorem 4 1 Form of Fz t The value returned by Fr t is a set of elements of the form d gt a p d gt cp d gt e v Theorem 4 2 Well definedness Fg t is well defined for substitutably guarded HyPA models Theorem 4 3 Soundness termination Termination in Fg t implies that t E can terminate i e lld gt V E Fet A d gt e vy gt t v v Theorem 4 4 Soundness transitions All transitions in Fg t can be performed by t E i e Sas d gt 2 8 Folt d gt 2 0 gt s 0 gt t 0 5 8 0 Theorem 4 5 Completeness termination Termination of t E is in Fr t i e bo gt 3g d gt e V Felt A d gt v V Theorem 4 6 Completeness transitions Every transition of t E is in Fg t i e tv gt 1 0 gt Fae d gt x t Fg t A d gt 2 v gt s u 4 1 2 Simulating other classes of HyPA models Next to substitutably guarded models we would like to simulate all guarded models definition 2 10 and possibly even unguarded models Soundness and well definedness have to be maintained Completeness is dropped because infinitely many states may be reachable by a given transition in a not substitutably guarded model 4 1 2 1 Guardedness The definition of guardedness allows for models that can be rewritten into s
52. able when modeling two flow clauses executing one after the other since the behavior of flow clauses is ongoing and never terminates The left disrupt is mainly needed for calculation and axiomatization purposes rather than for modeling purposes For example it occurs often when we attempt to eliminate the parallel composition from a process term through axiomatic reasoning as described in section 2 2 The left disrupt p gt q first executes a part of the process p and then behaves as a normal disrupt Parallel composition The parallel composition p q models concurrent execution of p and q The intuition behind this concurrent execution is that discrete actions are executed in an interleaving manner with the possibility of synchronization while flow clauses are forced to synchronize and can only synchronize if they accept the same solutions The synchronization of actions takes place using a partial commutative and associative communication function y Ax At A For example if the actions a and a synchronize the resulting action is a aya Actions cannot synchronize with flow clauses and in a parallel composition between those the action executes first This communication function is considered a parameter of the theory As with the left disrupt the operators left parallel composition and forced synchronization are mainly introduced for calculation purposes The left parallel composition p q models that either p performs
53. an instance of the corresponding 62 5 2 Input file format Table 5 5 ClauseFormalism methods getClauseFormalism name Given a clause formalism name returns a subclass instance solve transition Solves the given transition getFactory Returns a Factory object subclass The method is used during the parsing of an input file to select the proper clause formalism The getFactory method returns a new Factory instance for the formalism The Factory class is described in setion 5 1 3 5 5 2 Input file format Requirement 1 states that the input file format of the linearization tool must be read by the simulator However it turns out that this format does not provide the simulator with all the information that it needs Therefore we extend the format in the following ways Design decision 5 20 Variable declarations Variables need to be declared There are two reasons for this decision 1 Declaration of variables gives the simulator the opportunity to check for misspelled variable names in jump sets 2 In many formalisms variables cannot be distinguished from constants and functions To make the distinction variables need to be declared Design decision 5 21 Right associative gt operator The reinitialization operator is right associative but the linearization tool reads it left associatively The simulator follows the HyPA definitions and reads it right associatively Design decision 5 22 Clause formalism decla
54. are indicated with red arrows 1 The toolbar containing buttons for controlling the simulation and visualizations 115 Chapter F User manual Figure F 1 HyPAsim user interface 0ld puaba7 a U 9 loareaedua WA 5 S3910YI 116 F 3 User interface Figure F 2 HyPAsim toolbar El 1 xT xv G C auto adjust plats fan transitions 23 4 5 6 7 8 9 10 11 12 131415 16 The choices box where all currently possible transitions and their solutions are shown The legend showing the color that each model variable has in the plots and the current value of each model variable The actions viewer showing the performed actions against a time line The plots pane where the model variable behavior is shown in X T or X Y plots Figure F 2 gives a closer view of the toolbar Note that during actual simulation some but tons may be grayed out to indicate that they cannot be pressed at this time Here is a short description per button a longer explanation is in the next sections l 2 3 10 11 12 13 14 15 16 Load a HyPA model from a file Enter initial values for the model variables Enter additional predicates for the selected transition Solve the selected transition Solve all transitions Undo the last performed transition Stop random simulation Perform the selected transition Star
55. are not visible in the transition system That is why the arrow in the conclusion is labeled with my w 4 44 4 2 Additional HyPA operators instead of simply w Furthermore the semantics is chosen such that the valuation of hidden model variables does not change during an action transition The reason for this choice is that in the existing semantics of HyPA the valuations of model variables also do not change during an action transition Rule 33 describes the case for a continuous flow transition This rule is similar to rule 2 Note however that the valuation in the resulting state is equal to the last valuation of the flow Again the reason for this choice is that in the existing semantics of HyPA this is also the case Rules 34 to 36 define the actual abstraction operator in terms of the auxiliary abstraction operator Note that the local state variable v in the hypotheses of these rules is an arbitrary valuation whose domain is V A partial axiomatization is given in Table 4 4 In these axioms Var x denotes the set of free variables in the term x Table 4 4 only gives some basic axioms and some axioms that are necessary for the linearization algorithm Table 4 4 Axioms for the abstraction operator VlelellVlyll I Vize y VA1 Viz oj Viy e Vizo V true gt y VA2 Vjal gt Viv Veo V true gt y VA3 V On x amp On V x Jl VA4 VIEW I x VUW e VA5 Vlx
56. at the current water level on a regular basis and opens or closes the valve depending on the measured water level Some changes were made to the model after taking it from 7 The nothing action is in troduced to make the model substitutably guarded Furthermore the behavior of steam is now specified This lessens the interaction that is needed between user and simulator during simulation The results of a simulation session with the boiler model can be seen in figure 7 1 The top plot shows the inflow the bottom line and the water level the saw tooth shaped top line The bottom plot shows the controller clock You can see by the open close and nothing actions that the controller makes a decision each time the clock reaches the value of clockPeriod The simulator shows a shortcoming of the model itself Dependent on its initial value the water level can become negative This shows that the simulator can indeed be useful to correct some obvious mistakes in a model before the application of formal analysis tools Because this was the first model to be simulated it has served mainly as a test for the user interface We adapted colors font sizes placements of value labels on plot axes etc according to experiences with this model Also the model shows that the choice of solving clauses numerically or symbolically impacts the model itself For numeric calculation the construction clock clock H
57. ates This has to be communicated to the user Design decision 5 15 There is a hierarchy of interfaces for solutions to the different types of clauses as outlined in figure 5 11 The ISolution interface represents underspecific solutions and is little more than a description The other interfaces deal with specific solutions and they specify methods for retrieving values to plot and maximum time lengths in case of flow solutions Figure 5 11 Solution interface hierarchy interface ISolution interface ISpecificSolution A interface interface IFlowSolution IReinitSolution 5 1 3 5 Factory As it turns out each clause formalism needs its own subclasses of transitions clauses values and times However these are instantiated in other parts of the simulator than the clause formalism part see 5 1 4 4 Therefore we use the Factory class pattern 8 59 Chapter 5 Design Design decision 5 16 Abstract Factory class Each clause formalism has its own Factory subclass The whole application can access this class to create transitions clauses values and times specific to the current clause formalism 5 1 3 6 Exceptions A couple of exception classes were created to distinguish simulator exceptions from regular Java exceptions They are listed in table 5 3 and figure 5 12 As with Java exceptions are divided into regular and run time exceptions Regular exceptions must be caught and handl
58. ation the simulator calculates the set of first transitions and then starts to solve all transitions If there are many transitions this can take long This setting is a maximum on the time spent solving After this time control is returned to the user to solve transitions manually Choose maximum time in random simulation When this box is checked the maximum pos sible time will be chosen for each flow transition during random simulation This can mean a huge performance improvement since half flow transitions are usually not interesting Ignore zero length flows during random simulation Checking this box prevents the simu lator from choosing flow transitions that have a zero time length when there is an alternative The Mathematica tab allows the user to enter the mathematica kernel to use Usually the kernel is located in C Program Files Wolfram Research Mathematica 5 1 MathKernel exe The Visualization tab shows the same options as drop down box 16 see section F 7 2 4 but also allows for entering the time interval for the Fixed interval option F 9 Building If you want to build your own executable from the source code you need JBuilder 2005 JavaCup 0 10 and Mathematica 5 1 Open JBuilder open the project hypasim jpx First you need to change some settings Click Project Project properties Required libraries Click the javacup item and click Edit On the Class tab enter the main directory of
59. ause A re initialization v v R is defined to be a solution of a re initialization clause d D denoted v v d as follows e v v E V P if v v E P and for all x g V we find v x v x e v v Ed v d if v v Ed or 1 1 E d e vv d d if v v Ed and vv Ed e v v Ed d if there exists v Val with v v d and v v H d e 1 1 Ed if v v and there exists v Val with v v E d e v v E Cimp if there exists c X such that 1 0 E c and 0 0 v 4 If we have two re initialization clauses d d D the clause d d accepts exactly those solutions that are a concatenation of the re initializations of d and d The clause d does not change the value of any of the variables it just models the condition under which d has a solution The clause Cjmp imitates the re initializations performed initially by a flow clause c Obviously the re initialization clause false has no solutions while Vm true has every possible re initialization as a solution Note that true exactly allows all re initializations that do not change any of the variable valuations The semantics of the HyPA constants and function symbols is given in the tables 1 5 using deduction rules in the style of 12 In these tables p p q q denote process terms a a a denote actions c denotes a flow clause d denotes a re initialization clause H denotes
60. bounces only become smaller and smaller For the simulator this means that the length of the transitions becomes shorter and shorter For numeric simulation this model is difficult because at some point the time lengths become shorter than the presicion accuracy of the calculation In practice the ball eventually bounces to the same height every time 7 4 Billiards This example is taken from 17 It shows a ball bouncing around a billiards table There are variables mx and my representing the size of the table vx and vy representing ball speed in the two directions and x and y for ball position Initially the ball is somewhere on the table and it already has some speed The model from 17 is extended table 7 4 so that the ball stops eventually There is a constant P that models the friction between the ball and the table This causes the velocity of the ball to drop When a certain minimum speed is reached the model goes into a state in which the speed is actually zero T8 7 4 Billiards Figure 7 2 Thermostat simulation results 0 2 000 4 000 6 000 8 000 10 00 12 00 ff on off on off n ff on off jon Value Variable temperature versus time 30 00 28 00 26 00 24 00 22 00 20 00 18 00 16 00 14 00 12 00 10 00 8 000 6 000 4 000 2 000 D 2 000 4 000 6 000 8 000 10 00 12 00 Time sn Table 7 3 Bouncing Ball model A Vin altitude speed
61. capable of simulating a number of classes of HyPA models At least one clause formalism should be implemented that supports certain classes of differential equations in the predicates The simulator was to visualize process behavior i e the actions and the model variable jumps and flows Two modes of simulation were required step wise and random To ease simulation of models that have been created for the HyPA linearization tool the input file format of that tool should be read by the simulator Also the simulator should be able to cope with model variables for which behavior is not completely defined The simulator was to be modular with respect to file formats and clause formalisms A simulator has been built and it fulfills most requirements A simple but adequate develop ment process was used to gather requirements design and implement the simulator Case studies were performed several times during the process to gather more requirements and to test the simulator Classes of HyPA models The simulator repeatedly calculates the first possible transitions of a HyPA model To do so we defined an inductive function on the structure of the model Showing soundness of the function i e that it only produces transitions that the model can perform was easy since the function is based on the HyPA operational semantics Completeness and termination were proven for the class of substitutably guarded HyPA models The required HyPAj and HyPA c
62. d HyPA The idea behind this class is that the num ber of parallel processes stays the same throughout the simulation The definitions of HyPAjin models and HyPA models can be found in appendix B 21 Chapter 3 Requirements ID 1 Priority 1 Description The input file format of the linearization tool from 18 can be read Motivation You do not want to rewrite a model just so that it can be input into two different tools Therefore the simulator must be able to read models written for the existing tool Status Partially fulfilled The file format that the simulator reads is the same as that of the lineariza tion tool with some extensions that could not be avoided see section 5 2 Therefore a file written for the linearization tool will have to be extended with some additional declarations before it can be simulated ID 16 Priority 1 Description HyPA models in linear form definition B 1 without variable abstraction can be simulated Motivation Linearized models are perceived as easy to simulate since virtually no calculation of possible transitions needs to be performed Because there already is a linearization tool this would be a useful starting point for the simulator Status Fulfilled Any HyPA specification can be simulated and therefore linear ones as well For the class of substitutably guarded models definition 2 12 the simulator even finds all possibl
63. d systems Technische Univer siteit Eindhoven 2002 94 Appendix A Mathematical definitions The following definitons were taken from 10 Definition A 1 Differential equation A differential equation is an equation that contains a derivative of an unknown function which we want to determine from the equation Definition A 2 Ordinary differential equation ODE A ordinary differential equation ODE is an equation that involves one or several derivatives of an unspecified function y of x The equation may also involve y itself given functions of zx and constants The word ordinary distinguishes such an equation from a partial differential equation which involves partial derivatives of an unspecified function of two or more independent variables Examples of ODEs are y cos x y 4y 0 ry y 2e y a 4 2 y An example of a partial differential equation is Ou S Pu T r Oy Definition A 3 Order of a differential equation We say that a differential equation is of order n if the nth derivative of y with respect to x is the highest derivative in the equation Definition A 4 First order differential equation A first order differential equation contains only y and may contain y and given functions of Many times we are only interested in a particular solution for a differential equation that satisfies initial conditions Definition A 5 Initial condition Let zo and yo be constants An initial c
64. de d w v v E d and v v E eand e v v OS rule 4 gives e gt e v v Induction p v v OS rule 4 gives t v v Rule 6 t 2 p 0 q d gt x t Fg p or d gt x t Fg q for some p q By induction and OS rule 6 Rule 7 t poq d d Ae d gt ev Fzg p e gt ev Fg q OS rule 4 and the definition of gives Iv w v v E d v v E e By OS rules 4 and 1 we get d gt e v v and e gt e v v Induction p v v and q v v OS rule 8 gives t v v Rule 8 t p gt q d gt e v Fz p for some p q By induction and OS rule 11 Rule 9 t p gt q d gt e vV Fg p for some p q By induction and OS rule 11 Rule 10 t p q d d Ae d gt e v Fg p e gt e v Fg q OS rule 4 and the definition of gives Iy v v E d v v E e By OS rules 4 and 1 we get d gt e v v and e gt e v v Induction p v v and q v v OS rule 15 gives t v v 100 C 2 Fg t is sound Rule 11 t p q for some p q By construction the hypothesis does not hold Rule 12 t p q for some p q Analogous to Rule 10 Rule 13 t Og p By induction and OS rule 22 Rule 14 t X By induction and OS rule 23 101 Chapter C Proofs for Fr t Theorem C 4 Soundness transitions All transitions in Fg t can be performed by t E To prove Sas d gt gt x t Folt A d gt 2 4 gt s v gt
65. e lastgatepos 2 t 0 Qs t Quas true and false Boolean operators V gt 23 Chapter 3 Requirements 3 2 2 2 Requirements about clauses We choose differential equations and inequalities for a clause formalism Differential equations are a natural way to describe many physical processes We anticipate the use of mathematical solvers such as Mathematica Matlab or Maple to solve the equations Different types of differential equations are described in appendix A These definitions are used in the following requirements ID 35 Priority 1 Description The simulator can handle equations between the derivative of a model variable and other model variables and constants e g w v s in flow clauses Motivation For a first version of the simulator we like to keep the equations simple Status Fulfilled ID 36 Priority 1 Description The simulator can handle equations between model variables and constants as flow predicates and reinitialization predicates Motivation For a first version of the simulator we like to keep the equations simple Status Fulfilled ID 20 Priority 10 Description The simulator can handle first order linear differential equations in the flow clauses definition A 7 Motivation First order linear differential equations are particularly easy to solve the answer is of a fixed known form and al
66. e transitions The currently implemented clause formalisms however do not allow for cjmp constructs in the reinitialization clauses ID 43 Priority 15 Description HyPA models can be simulated Motivation Models of the form HyPA frequently occur and simulation of these models is anticipated to be simpler than simulation of guarded models in general see section 4 1 Status Fulfilled Any HyPA specification can be simulated and therefore the class HyPA as well For the class of substitutably guarded models definition 2 12 the simulator even finds all possible transitions The currently implemented clause formalisms however do not allow for Cjmp constructs in the reinitialization clauses ID 46 Priority 16 Description HyPA models with variable abstraction can be simulated Motivation It is useful that the simulator can read models with abstraction so that the abstractions need not be removed specifically for simulation Variable abstraction does become less useful in simulation as explained in section 4 2 4 2 Status Partially fulfilled For reasons also described in section 4 2 4 2 the simulator only supports one abstraction operator at the beginning of the model This is enough to simulate the HyPA models that can be read by the linearization tool Therefore models that are intended for analysis do not have to be rewritten for simulation 22
67. ed by the application Run time exceptions mainly method precondition checks are not expected to occur and are not handled by the application Table 5 3 Exceptions EHyPASimException Base class for all simulator exceptions EHyPASimRuntimeExceptions Base class for all simulator run time exceptions EHSParseException Parsing exception syntax errors undeclared actions etc EHSSolveException Exception thrown by the clause formalisms EHSWrongOrderException Thrown when methods are called when they should not be Figure 5 12 Exceptions hierarchy RuntimeException A LN EHyPASimException EHyPASimRuntimeException 5 7 EHSParseException EHSSolveException EHSWrongOrderException 5 1 4 Engine The engine has the tasks of parsing input files calculating first transitions and solving clauses The division of the engine into sub packages and classes is based on these tasks and on the extensibility requirements The engine needs to be extensible in several respects Requirement 60 5 1 Architecture 2 states that it should be simple to add another input file format Requirements 4 19 and 23 require extensibility with respect to the clause formalism Figure 5 13 Engine static structure RealEngine ModelParser ClauseFormalism A format1 mmaformalism ModelParser1 MmaClauseFormalism Figure 5 13 s
68. ended version of Fz t is well defined Theorem 4 12 Soundness termination Termination in the extended version of F r t implies that t E can terminate i e lld gt ev Fa t A do e v v gt t u v Theorem 4 13 Soundness transitions All transitions in the extended version of Fg t can be performed by t E i e Sas s d29 2 8 Felt A d gt 2 0 gt s v gt t 0 gt 8 0 Theorem 4 14 Completeness termination Termination of t E is in the extended version of Fr t i e tv gt Il ld gt e V Fg t dz e v v Theorem 4 15 Completeness transitions Every transition of t E is in the extended version of Fz t i e tv gt 1 0 gt Sas s d gt x t Fg t A d gt 2 4 gt s u 4 2 4 Model variable abstraction Peter van den Brand has defined a model variable abstraction operator in 18 chapter 5 First we give the original definitions Then we describe the extent of the support for the operator in our tool 43 Chapter 4 Analysis 4 2 4 1 Definitions For ease of reference we repeat the definitions of model variable abstraction from 18 Chapter 5 We re number the OS rules to distinguish them from the other HyPA OS rules The remainder of this subsection is from 18 In table 4 3 the semantics of both types of abstraction operators is given To keep the rules concise the auxiliary functions my y v and my 0 0 are used which me
69. equirements completeness for other classes of models and useful additions to the simulator Unfulfilled requirements include e Implementing a generic clause formalism to which different solvers can be connected but this is restrictive to the user e A different way of indicating steps to undo 90 e Having a predicate as a stop criterium for random simulation e For other input file formats to be read there must be some selection mechanism for input formats in the user interface e Simulation of models with abstraction anywhere e Filling in random behavior for unspecified behavior In order to prove completeness of the first transitions function one of the two failed approaches to the function can be explored further The protectedness property section 4 1 2 1 can be in vestigated further to match bounded non determinism to a structural property of a model Also another way of proving the fixpoint approach section 4 1 2 2 could be tried Additions to the simulator could include e Providing more information to the user on underspecific clauses e More error checking of clause predicates e Having a new operator to rename constants within a clause predicate e Having simulator settings for a model in a file per model 91 Chapter 8 Conclusions 92 Bibliography 1 R Alur R Grosu Y Hur V Kumar and I Lee charon a language for modular specification of hybrid systems Technical report University of
70. erators is limited 5 3 2 Mathematica clause formalism The mathematica clause formalism is meant to give the user the freedom to specify most of what Mathematica allows Predicates consist of differential equations and inequalities in Mathematica notation Numerical methods are used to solve the clauses This decision is backed by the fact that more differential equations are solvable by numerical methods than by symbolic methods Identifiers Variables and constants may have any name that Mathematica allows except for t The name t is used as a independent time variable for the differential equations Using lowercase letters ensures that a name does not coincide with an existing Mathematica symbol Definitions Constants can be defined in a def section They are given as lt name gt lt value gt constructs separated by semicolons The names must be valid unique identifiers and the values must be Mathematica Real literals Example def wMin 3 wMax 6 0 Flow predicates Flow predicates consist of e differential equations that specify continuous behavior over time The symbol is used to specify an equation Differential equations must be stated in the form that is understood by the Mathematica NDSolve function Initial and boundary conditions are typically stated in form y to Co y to dco etc but may consist of more complicated equations There must be exactly enough i
71. es The set 7 V denotes the set of all terms in which only recursion variables are used Such elements are referred to as process terms We only allow recursive definitions X p where the term p is a process term Outside the recursive specification recursion variables are treated as constants of the theory Recursion is a powerful way to model repetition in a process The binding order of the operators of HyPA is as follows gt gt d gt where alternative composition binds weakest and sequential composition binds strongest With encapsulation Oy _ brackets are always used As an example a term d gt a b cl c should be read as d gt a b e c 2 1 1 Formal semantics In this section we give a formal semantics to the syntax defined in the previous section by constructing a hybrid labeled transition system for each process term and each possible valuation of the model variables The hybrid transition systems we use here have two different kinds of transitions one associated with computational behavior i e discrete actions and the other associated with physical behavior i e flow clauses There is also a termination predicate v on states indicating successful termination of a computation Furthermore we have adapted the notation in this chapter to the notation that is more commonly used in the development of process algebras The system structure is indicated by two separate transitio
72. for some p p d We have two cases e Case 1 x a d gt a p Fg p for some a By OS rules 2 and 5 we have that a v and v v E d By the extra assumption we have that V 1 v V 1 v Ed and thus d gt a V 1 y 55V 0 e V 1 0 By induction we get p V 1 v V p V 1 v By OS rule 29 we get t v 3 t v e Case 2 x V c Ld gt cp Fg p for some a By OS rules 3 and 5 we have that l c and v v E d v 0 E V c dom o 0 t v e t for some v c t By the extra assumption we have that V 1 v V 1 v E d V 1 v V e c and 107 Chapter C Proofs for Fg t thus d gt c Veto Vot Ce V 1 a t By induction we get p V 1 v Voto pl Vlo By OS rule 30 we get t v Zul 0 Theorem C 11 Completeness termination Termination of t E is in the extended version of Fg t To prove bu gt da d gt e Felt do e v v Proof Extend the proof of theorem 4 5 with the following OS rule 25 t palp for some A p and p v v By induction d4 d gt vV Fg p d gt v V Therefore by definition of Fg pA p we have Ja d gt e v Felt A d gt e v v OS rule 28 t oy p for some V p and p v v By induction Ja d gt e Y Fg p d gt v V Therefore by definition of Fr ov p we have Ja d gt e v Fg t A d gt e v v Theorem C 12
73. he interface between user interface and engine in this section This interface consists of an abstract class for accessing the engine representations for transitions process terms solutions 52 5 1 Architecture Figure 5 6 First transitions communications VisualizationManager SimulationManager Engine getFirstTransitions getFirstTransitions gt first transitions K MODERN solve transition gt solutions o cea solve transition gt solutions transitions and solutions pee K EEE 53 Chapter 5 Design Figure 5 7 Random simulation communications VisualizationManager SimulationManager RandomThread Engine i start start ok ok See Paste to aa getFirstTransitions transitions transition performed stopped transition performed stopped 54 5 1 Architecture times and values and exceptions Each is described below 5 1 3 1 Engine facade In order to be able to test the user interface before implementing the rest we define an interface through which all communications to the engine take place This single access point to the possibly complicated engine is also known as a Fagade 8 It creates the possibility of attaching a dummy engine or a real engine depending on what we want to tes
74. hitespace Examples 64 5 2 Input file format comm ropen sopen open rclose sclose close comm ala b alb c Combined action communication declarations Action declarations and communication declarations can become cumbersome to write Therefore the keyword actcomm is introduced which allows you to declare actions and their communications in one statement of which you may write zero or more in your model Examples actcomm ropen sopen open rclose sclose close actcomm ala b alb c This declares the actions ropen sopen open as well as the communications y ropen sopen open etc Process equations Each process definition X p is described by a section of the form proc X p where X is the name of a recursion variable and p a process term Example proc X a X b Y Initial process There is one initial process term defined by initial proc X p In accordance with the file format of Requirement 1 this defines the initial term p as well as the definition X p Terms The mapping of HyPA constructs to ASCII constructs is described in table 5 6 Note that brackets are used solely for grouping not for flow clauses Operator precedences are from strong to weak gt gt gt Il L 9 and V cmp and L All operators are read left associatively except for and gt which are read right associatively For variable renaming 0 7y y 2 p right arrows x gt
75. hows the structure of the engine The RealEngine facade class implements the Engine interface It uses instances of two abstract classes ModelParser and ClauseFormalism to do the calculations 5 1 4 1 State The RealEngine class records the current and previous states These states are represented by the State class and consist of the current specification process term valuation and the current time The terms are represented by trees of HyPAElement objects 5 1 4 2 Parsing The simulator has to be extensible with new input file formats 61 Chapter 5 Design Design decision 5 17 Abstract parser class There is an abstract ModelParser class that specifies a parser The parser takes a file and returns a HyPASpecification object This HyPA specification consists of the process equations the initial term the communication function y etc All terms are represented as a tree of HyPAElement instances For each different input file format there is to be a subclass of ModelParser Currently there is only one format format number 1 described in section 5 2 Its associated subclass is called ModelParseri As it turns out the input file format is ambiguous In particular the parser cannot determine in one pass the difference between flow and reinitialization clauses and between actions and recursion variables T herefore this parser has two stages in the first stage a simple tree derived from HE1Element is created In the second
76. igure F 4 Underspecific clauses Possible transitions D a 2 Underspecific xP 0 2 Vm True True Underspecific add more equations Sometimes the clauses in a model are not specific enough to be solved For instance the flow clause S Sup S8 Xmas does not specify actual solutions for s In this case solutions are shown in the choice box with a preceding question mark like in figure F 4 You can double click the solutions or press button 3 to add predicates that make the clauses more precise F 5 2 Choosing a solution From the solutions in the choice box you have to choose one to perform You do this by clicking it Note that all visualizations show the past behavior and the selected solution In case of a flow you also have to choose a time length for the transition The X T plots will show a blue vertical bar Using the mouse you can drag this bar left and right to select the length of the flow Once you have chosen a solution and possibly a time length you can click button 8 to per form it Double clicking the solution also works In case of deadlock the simulator presents an empty choice box F 6 Random simulation The simulator can make all choices on its own You can start random simulation by clicking button 9 Most buttons except for the stop button number 7 are grayed out The visualizations are updated periodically The frequency of these updates is once a second but can be delayed somewhat by
77. in Fg t To prove tv gt 8 0 gt dae d gt x t Fg t d x u gt s v Proof Proof by induction on the length of the derivation of t v t v We make no distinc tion between base and step cases We use case distinction on the OS rule applied in the last step in the derivation OS rules 1 4 6 8 11 13 15 22 23 do not produce transitions so we only need to take the other rules into account We use theorem 4 5 Completeness termination OS rule 2 t a for some action a and the definition of Fg a combined with axiom 9 1 im plies Jg d gt gt z t Fg t A d o 2 4 5 s v Y OS rule 3 We have that t and t are equal to a flow clause c Thus Fg t Fg c true gt c c Since according to axiom 9 1 we have that true gt c c we have Jas d gt v t Felt d gt 2 0 gt s v OS rule 5 We have for some d p p v that t d gt p and p and v v E d and p v p v By induction we have that ders Ce gt x t Fg p le gt x u gt s v There fore we have 3 v v E e and thus v v E d e Now by OS rule 5 and the definition of Fg t we have Jaz o d gt z t Felt A d gt 2 4 5 s v OS rule 7 For some p q we have that t p q and either p v t v or q v gt t v By induction we have Jaz d gt x t Fg p d gt 2 0 gt s v
78. inland 2004 IEEE Computer Society Press 12 G D Plotkin A structured approach to operational semantics Technical Report DAIMI FN 19 Computer Science Department Aarhus University 1981 13 Ptolemy plot URL http www ptolemy eecs berkely edu java ptplot index htm 14 R R H Schiffelers D A van Beek K L Man M A Reniers and J E Rooda Formal seman tics of hybrid chi In Kim Guldstrand Larsen and Peter Niebert editors Formal Modeling and Analysis of Timed Systems FORMATS 2003 volume 2791 of Lecture Notes in Computer Science pages 151 165 Springer Verlag 2004 15 Alfred Tarski A lattice theoretical fixpoint theorem and its applications Pacific Journal of Mathematics 5 285 309 1955 16 Y S Usenko Linearization in CRL PhD thesis Technische Universiteit Eindhoven 2002 93 BIBLIOGRAPHY 17 D A van Beek K L Man M A Reniers J E Rooda and R R H Schiffelers Syntax and 18 19 20 consistent equation semantics of hybrid chi Technical Report Computing Science Report 04 37 Eindhoven University of Technology Department of Mathematics and Computing Science 2004 P C W van den Brand Linearization of hybrid processes Master s thesis Technische Uni versiteit Eindhoven 2004 P C W van den Brand M A Reniers and P J L Cuijpers Linearization of hybrid processes Journal of Logic and Algebraic Programming 2005 Huub van den Broek Practical assignment Visualizing hybri
79. ion A HyPAyn specification is a recursive specification t E that satisfies the following three restric tions 1 t E is substitutably guarded definition 2 12 2 t is in HyPApar form and 3 the right hand sides of all recursive equations in E are in HyPAjy form Definition B 3 HyPA pa Form The HyPA par form is defined as the form p I Vlall 4 a X alla r g 97 Chapter B Input restrictions Definition B 4 HyPA rin Form The HyPAjyin form is defined as follows p a X amp c pep pop d gt p p et HyPA input restriction A HyPA specification differs from a HyPAin specification in that abstraction is no longer allowed and that parallel processes cannot terminate Definition B 5 HyPA Specification A HyPA specification is a recursive specification t E that satisfies the following three restric tions 1 t E is substitutably guarded 2 t is in HyPA form and par 3 the right hand sides of all recursive equations in E are in HyPAft form Definition B 6 HyPA Form par The HyPA form is defined as the form q par q X alla On a Definition B 7 HyPAj Form The HyPA form is defined as the form p lin p X c per 40X dep cp cb q a X 6 c aaqa ada dea ara gh a 98 Appendix C Proofs for Fp t Here the first transitions function Fr t defined in section 4 1 1 is proven correct Fir
80. ith medium priorities Prio ID St Description 4 12 F Random simulation is possible where all choices are made by the sim ulator The visualizations are updated continuously The simulation is stopped on deadlock and on user command 4 44 F The stop criterium can be the occurrence of a given action 5 4 N Another differential equation solver can easily be used 6 23 F The system is extendable with a mode for numerical instead of symbolic computation T 52 F The jumps in model variable values are visualized when an action transi tion is chosen but not yet performed 8 13 F The user can undo steps whenever the simulation is stopped 9 28 N The number of steps to undo can be indicated by the user in the X T plots Table 3 3 Requirements with low priorities Prio ID St Description 10 20 F The simulator can handle first order linear differential equations in the flow clauses 11 3T F The simulator can handle inequalities in flow clauses and reinitialization clauses 12 45 N The stop criterium can be a predicate on the model variables 13 41 F The user can indicate that the maximum possible time interval is chosen for every flow transition in random simulation mode 15 43 F HyPA models can be simulated 16 46 P HyPA models with abstraction can be simulated 17 22 F The relation between two model variables can be visualized in an X Y plot 17 27 F A legend can be shown in which each model variable
81. king version have shown that we do not want the X T plots in separate windows Apart from that the requirement is not really verifiable 30 3 3 Requirements sorted by priority 3 3 Requirements sorted by priority In tables 3 1 3 2 and 3 3 the requirements are listed by their priority Deleted requirements are not in the table The third column indicates the current status of the requirement N Not implemented P Partially implemented or F Fully implemented Priorities are assigned based on two criteria Firstly requirements should be independent of requirements with a lower priority Secondly the priorities are such that a system that meets the higher priority requirements is relatively simple to build and yet usable The combination of the requirements with priorities 1 through 3 yields a system that can perform step wise simulation on linearized HyPA specifications that have relatively simple equations in the clauses The re quirements with priorities 4 through 9 specify features that make the simulator more convenient to use with random simulation and undo possibilities The lower priority requirements make the system more technically difficult with more complicated clause formalisms and less restricted HyPA models Table 3 1 Requirements with the highest priorities for a first working version Prio ID St Description 1 1 P The file format of the linearization tool from 18 can be
82. l have a closed interval domain starting in 0 The flows that are described by a flow predicate are called solutions of that predicate We consider the set of flow predicates Pr the sets Vm of model variables and T of time points and the notion of solution lt r C F x Pr that defines which flows are considered solutions of a flow predicate parameters of our theory This means they can be instantiated by the modeler depending on the specific modeling or analysis problem The theory we present in this chapter is largely independent of that choice except that we assume the existence of a flow predicate false P that satisfies no flow from the set F An atomic flow clause finally is a pair V Pr of a set of model variables V C Vm signifying which variables are not allowed to jump at the beginning of a flow and a flow predicate Pr P modeling continuous never terminating physical behavior The set of all flow clauses is denoted C We usually leave out the brackets for V and even omit it and the delimiter if it is empty Furthermore the set C is closed under conjunction A of flow clauses and using the assumption that there is a flow predicate false which is never satisfied there is also a flow clause false which is the system theoretic equivalent of deadlock 6 Re initializations As with continuous physical behavior there are several formalisms in systems theory that deal with discontinuous physical behavior and agai
83. lasses of models are contained in the class of substitutably guarded models The simulator exceeds the requirements by allowing all possible HyPA models to be simulated It does not guarantee completeness for models outside the substitutably guarded class An artificial termination criterium for the calculation is introduced through which the user can indicate how much effort to spend to find first transitions Extensions to HyPA HyPA models can become cumbersome to write in particular when many sub processes are similar To solve this new HyPA operators have been defined and the simulator allows for some syntactic sugar in its input format The new operators are action renaming and variable renaming They are defined through operational semantics Robust bisimulation is proven to be a congruence for them so the HyPA derivation system is still correct for HyPA models that use them The syntactic sugar comprises easier declaration of actions and communications notation for the entire set of model variables and notation for all the halves of the communications Model variable abstraction is implemented only partially and this is similar to the state of affairs in the linearization tool 89 Chapter 8 Conclusions Clause formalisms The simulator implements two clause formalisms both related to Mathematica One solves the clauses numerically and the other symbolically A generic clause formalism that allows for any solver to be u
84. mathematica and the symbolicmma clause formalisms section 5 3 These formalisms use every possibility that Mathematica has to offer but they are hardly implementable on other solvers Needed is a clause formalism in which a general syntax is defined which is then translated to syntax that the different solvers understand We once started working on such a formalism section 5 3 1 but we abandoned it because of the inherent limitations on its expressiveness ID 23 Priority 6 Description The system is extendable with a mode for numerical instead of symbolic computation Motivation Numerical solving of differential equations allows for a larger class of equations to be solved Status Fulfilled ID 19 Priority 20 Description Another clause formalism can easily be added Motivation HyPA does not define the formalism used in the clauses The usability of the solver would be prolonged if new clause formalisms could be added to it Status Fulfilled Addition of a class and a factory method is all that is needed to add a new clause formalism 29 Chapter 3 Requirements Deleted requirements ID 33 Priority 1 Description The simulator can easily be changed to one that displays each plot in its own window Motivation Some simulators for other hybrid formalisms use separate windows Status Deleted The prototypes and the first wor
85. n the modeling or analysis question determines which formalism is to be used in a specific situation In general one may say that discontinuous behavior is described through predicates about the re initialization or discontinuity or change of variables As an example of such a predicate consider a difference equation z f x7 u7 which denotes that the value of x is reassigned to f x u based on the previous values of x and u Re initialization predicates describe a set of re initializations which are pairs of valuations representing the values of the model variables prior to and immediately after the re initialization Such re initializations are called solutions of the re initialization predicate The set of all re initializations Val x Val is denoted R As before the set of re initialization predicates 7 and the notion of solution EC R x P that defines which re initializations are considered solutions of a re initialization predicate are considered parameters of the theory We assume the existence of re initialization predicates true false P that satisfy any re initialization and no re initialization from the set R respectively A process re initialization d gt p models the behavior of p where the model variables are submitted to a discontinuous change as specified by the re initialization clause d A re initialization clause is a pair V P of a set of model variables V C Vm and a re initialization predicate P The set V
86. n relations C X x Ux X and C X x A x X Definition 2 1 Hybrid Transition System A hybrid transition system is a tuple X A Y ne v consisting of a state space X a set of action labels A a set of flow labels Y and transition relations C X x Ax X and C X x Xx X Lastly there is a termination predicate Y C X For the semantical hybrid transition systems that are associated with HyPA terms the state space is formed by pairs of process terms and valuations of the model variables i e X 7 V x Val The set of action labels is formed by pairs of actions and valuations i e A A x Val and the set of flow labels is formed by the set of flows ie F Recall that the elements f F have a closed interval domain possibly a singleton starting in 0 Let x 1 X be two states We use the notation x 5 a for a transition x a x with a A Similarly we use x a for a transition x 0 1 with o Y For arbitrary transitions we use 1 a z instead of a l x U with AUX Finally termination is denoted x v instead of x Y Before we turn to the actual definition of the semantics of HyPA in terms of hybrid transition systems a notion of solution for flow clauses and re initialization clauses is needed for the definition of the semantics of these atoms of the algebra These notions are obtained by lifting the notion of solution of flow predicates and re initializa
87. name is replaced by a user supplied name 20 7 N The current location in the original model text of each parallel process is visible 20 19 F Another clause formalism can easily be added 22 39 F The simulator can handle all differential equations that the solver tool can handle 25 47 F The simulator can handle ordinary differential equations 26 31 N The simulator can be set up so that it fills in a random function for a given unconstrained model variable 26 32 N The simulator can be set up so that it fills in a random continuous function for a given unconstrained model variable 32 Chapter 4 Analysis In this chapter we explore some aspects of simulating a HyPA model In section 4 1 we explore what HyPA models can be simulated and how to obtain the transitions that a model can perform Then we introduce some new HyPA operators that make writing models easier and that increase the efficiency of the simulator 4 1 First transitions A HyPA model determines a transition system through its operational semantics The simulator shows a trace through this transition system Since the transition system can be infinitely large we do not construct the entire transition system before picking a trace Rather we determine the outgoing transitions from the current state pick one and make the resulting state the current state Although this set of outgoing transitions can be infinitely large as well it turns out that we can desc
88. nism for any arbitrary number of steps e A process p has bounded non determinism denoted B p if for every valuation v Val we find that p v has bounded non determinism Van den Brand introduces a weaker definition of guardedness in 18 To distinguish it from the previous definition of guardedness we rename it to subtitutably guarded Definition 2 12 Substitutably guarded As in definition 2 10 an open process term p is guarded if all occurrences of process variables in p are in the scope of an action prefix a or a flow prefix c gt _ A recursive specification E is substitutably guarded if for each recursive definition X p E pis guarded or can be transformed into a guarded term by replacing variables by the right hand side of the equation The class of substitutably guarded specifications is contained in the class of guarded ones which in turn is contained in the class of bounded non derterministic specifications 17 Chapter 2 HyPA semantics and axioms Table 2 7 Axioms of HyPA part 1 LOY X yeu rez relye 2 LOT T LPWOz x xozeyosz xOyOz x O yO z LO T eOu ZT dOr 0 TOE mcm cor mc false t gt y x T U DU t y oz F ce zeyrpz gt r 6 rb y bz zm ar ym 2 D zr aOrP gt y a0 ap y EDT Ze z y zlyegyl zezly el x 6 ale m c aOoz y ao elly Lr G VLS xl 0 yl lt corly m sz zl 412 sle x lye ell 2 ele
89. nitial conditions to specify a single particular solution Initial conditions are also introduced by adding model variables to the jump set of the flow clause e Inequalities that specify conditions on the continuous behavior e g z 13 These inequali ties are solved by shortening the time domain of the solution to the equalities The symbols lt gt lt gt can be used to specify inequalities Conditions on the solutions of the equalities can be stated as e g x 100 which is taken to mean that the solution for x t must be less than 100 on its entire domain The simulator accomplishes such a condition by reducing the domain 69 Chapter 5 Design e Equations and inequalities are combined using amp amp e All model variables are treated as functions over t their domain ranging up from 0 No model variable may have name t e All existing Mathematica functions and constants may be used although NDSolve does not find solutions for every possible differential equation Notably the Sign function causes Mathematica 5 1 to crash when used within a NDSolve call e The predicates False and True may be used on their own as flow predicates A flow o Vm gt 0 t R is a solution to a flow clause if the equalities hold on the en tire domain 0 and the inequalities on the open domain 0 t Example x t x t y t amp amp y t 2 Sin t amp amp y lt Pi Reinitialization predica
90. nly Example clause formalism mathematica Definitions There may be zero or more definition declarations They start with the word def and between square brackets 1 global definitions for the clauses e g constants functions etc can be given These definitions are clause formalism specific Examples can therefore be found in section 5 3 that defines the clause formalisms Variable declarations There may be zero or more variable declarations Together they list all used model variables A variable declaration starts with the keyword var followed by one or more variable names Variables can be separated by whitespace or by commas Variables consist of a letter followed by letters and digits and may not be equal to any of the keywords The used clause formalism may impose further restrictions on the variable names Examples var water inflow outflow var water inflow outflow Action declarations There may be zero or more action declarations Together with the actcomm declarations see below they list all used discrete actions An action declaration starts with the keyword act followed by one or more action names Actions can be separated by whitespace or by commas Communication declarations There may be zero or more communication declarations that specify the communications function y They start with comm followed by triples alb c signifying that y a b c and y b a c Triples may be separated by commas or w
91. ns of equalities and inequalities over the previous and next value of the model variables A previous value is indicated by the name of the model variable followed by the letter P and a next value is indicated by the name of the model variable followed by the letter N All model variable occurrences must have suffix P or N The predicates False and True may be used Example xP lt 5 amp amp xN xP 10 72 Chapter 6 Implementation This chapter describes decisions made in the Implementation phase Detailed design documen tation is provided in comments in the code itself The comments use JavaDoc syntax so that documentation in HTML form is easily generated 6 1 Programming language We choose Java as a programming language for a number of reasons e Java is the only language with which all of the considered solver tools Matlab Maple Mathematica can communicate e Performance is expected to be more of an issue of the mathematical solver than of the simulator e Java offers garbage collection and compile time checks of exception declaration taking some concerns out of our hands JBuilder 2005 Enterprise is used as development environment since it is available at the TU e 6 2 Coding style We provide JavaDoc comments for obvious reasons We adhere to most of the coding guidelines that can be checked by the JBuilder Coding Audits They seem reasonable and can obviously be checked automatically JBuilder automatically
92. nsitions However in practice we cannot determine whether two processes are robustly bisimilar For ex ample the bounded non deterministic process 0447 X where X a X y a a c y a c y c a a and y c c c can with a c transition reach the syntactically different states e X el e X ele le 1 X All of these states are equivalent axiom number 7 9 In practice it prevents F from reaching a fixpoint and terminating This is not only a problem of the fixpoint approach but also of the original first transitions function The function returns a set and thus it should not return two bisimilar transitions In practice it does but it terminates anyway Some optimizations for this problem are described later in this chapter We abandon the fixpoint approach in favor of the maximum recursion depth approach described next 4 1 2 3 Maximum recursion depth The idea behind the maximum recursion depth approach is to allow any HyPA specification to be simulated and let the user determine how much effort to spend on calculating first transitions Well definedness of the first transitions function is trivial in this approach completeness is only guaranteed for substitutably guarded models We add a parameter to Fg t that indicates the number of times that F is applied to each recursion variable recursively Also we introduce a user specified constant nar that indicates the maximum allowed recursion depth Definition 4 8 F
93. nsitions are visible It applies to the action viewer X T and X Y plots There are four choices Last transition Time ranges are only adjusted when the last transition does not fit in In that case the range is set to twice the length of the last transition All transitions The time range is adjusted to fit all transitions Fixed interval The time range is set to a specific length The end of the time range coincides with the end of the last transition The length is a user specified setting section F 8 No adjustment Plots are not adjusted during simulation Each time you zoom or scroll a plot the auto adjustment option is automatically returned to No adjustment F 8 Settings There are several settings all accessible by clicking Tools Options A dialog with three tabs appears We list the settings per tab On the Simulation tab you can find the following settings Lookahead time Sometimes a flow transition can have any time length The simulator cannot cope with this so a maximum time length must be provided 122 F 9 Building Max recursion depth For models that are not substitutably guarded definition 2 12 the user must specify how much effort to spend on calculating first transitions This is achieved by setting a maximum on the number of times that the first transitions function may be calculated recursively for each recursion variable see also section 4 1 2 3 Max solve duration In step wise simul
94. o solving a transition Commands must be separated by semicolons This allows for example for the definition of constants and functions All expressions must be symbolic This implies that numbers with decimal points are not allowed Example def wMin 3 wMax 60 distance x1_ x2 Sqrt x2 x1 2 Flow clauses A flow predicate is either False True or a list of length 2 The list is enclosed by The first element consists of differential equations combined using amp amp The second element is any logical combination of inequalities The equations are solved by the DSolve function Inequalities are solved by Reduce t Reals All model variable occurrences must range over variable t Here is the formal definition of a solution to a flow clause Definition 5 1 Erf Let c be a continuous flow with domain 0 t for some t Let Py E I be a valid flow predicate over the model variables over time We define f as follows o Er Pr iff Viejo E t and Ve ero I t Note that on the upper border of the domain of c the inequalities do not have to hold This ensures that constructions like V z t 2 1 z t 3 3 gt a are possible 71 Chapter 5 Design Examples x t x t y t amp amp y t 2 Sin t y t lt Pi y tl gt Pi water t inflow t outflow t True Reinitialization clauses Reinitialization predicates are logical combinatio
95. on a class for each atomic HyPA element HEBinaryOperator i a class for each binary a class for each operator HEFClause on flow clauses MAA HyPA operator HEUnaryOperator HEReinitializationClause N a class for each unary HyPA operator a class for each operator that returns a reinitialization clause HERCIause 58 5 1 Architecture 5 1 3 4 Solutions times and values The representation of solutions times and values depends highly on the clause formalism used For example the numerical mathematica formalism uses real numbers while the symbolic math ematica formalism uses symbolic expressions However the user interface needs to make some basic assumptions about them in order to be able to draw plots and accept user input e Times can be converted to and from a positive real number e There is a reasonable conversion of values to a real number for representation in plots Design decision 5 14 ITime and IValue The ITime and IValue interfaces capture these assumptions Clause formalisms use different implementations of these interfaces For solutions an interface is needed for the user interface to retrieve values flows and max imum time lengths Also solutions can be underspecific when the behavior of a model variable is not sufficiently constrained by the clause predicates see also section 5 1 3 2 on additional predic
96. ondition is a predicate of the form y xo yo 95 Chapter A Mathematical definitions Definition A 6 Initial value problem An initial value problem is a first order differential equation together with an initial condition Definition A 7 First order linear differential equation A differential equation is called linear if it can be written y p x y r x where p and r may be any given functions of z Function p is called a coefficient of the equation Linear differential equations have a known general solution y x e f e rdx c where h peda 96 Appendix B Input restrictions Here different restrictions on HyPA specifications are described These restrictions are used in the requirements chapter 3 to specify which classes of HyPA models need to be simulated Linear Recursive Specification From 18 Definition B 1 Linear Recursive Specification A linear recursive specification t E is a recursive specification that satisfies the following re quirements 1 the initial term t is either a recursion variable in E i e X or the variable abstraction of a reinitialization on such a variable i e V dz X and 2 the right hand sides of all recursive equations in E are linear terms A term is linear if it has the BNF form p pr d d gt a d gt a0X deer X pop HyPA jin input restriction Here is the definition of a HyPAjin specification from 18 Definition B 2 HyPAj Specificat
97. ore solutions to the transitions as well The user interface retrieves the possible transitions from the engine and may request the engine to solve some or all of them After that the user must select the combination of a transition solution and a next process to perform Thirdly sometimes additional predicates are needed In many models intended for analysis the clauses do not completely specify the behavior of the model variables An example is the flow clause predicate Smin X X Smar In this case the user must enter some additional predicates to constrain the behavior of s for simulation These predicates are also stored in the Transition object Design decision 5 9 Transition class The Transition class represents a tuple p A N where p indicates the clauses and type of transition d gt a doc d gt e Aisa set of additional predicates N is a set of possible next process terms and S is a set of solutions to the clauses 56 5 1 Architecture Design decision 5 10 Transition hierarchy There are some differences between the three types of transitions and therefore a subclass is created for each of them The hierarchy can be found in figure 5 9 Figure 5 9 Transition hierarchy IN Termination FlowTransition ActionTransition 5 1 3 3 Process terms Throughout the application HyPA process terms must be represented Design decision 5 11 HyPA element hierarchy There is a hierarchy of classes
98. ot much emphasis is placed on following a specific software development standard The development process is based on an iterative waterfall model figure 1 1 There is a requirements phase during which user require ments are collected In the analysis phase miscellaneous areas of the problem are analysed The design phase captures the architectural design of the program There is no detailed design phase Detailed design is provided by structured comments in the code from which HTML documentation can be generated In the implementation phase elements from the eXtreme Programming paradigm 3 are used programming feature by feature and for the more complex parts of the program unit testing In the cases phase some models are simulated to serve as an integration test A maintenance stage is not provided for It is unlikely that the tool will gain widespread use or that there will be any human resources to provide maintenance for the tool All phases together form one iteration The simulator is developed in several iterations In the 5 Chapter 1 Introduction Figure 1 1 Development process phases Implemen tation Requirements gt Analysis Design Pb 8 be Cases Unit tests successive iterations emphasis shifts from the first phases to the final ones The first iterations are primarily for the collection of requirements After establi
99. out not to handle the case that the jump at the beginning of a flow clause is taken over by a reinitialization Cases The example models show that the implemented visualizations are indeed useful Also the addi tional HyPA operators turn out to be useful An additional renaming operator for constants in clause predicates could be useful as well Step wise and random simulation work as expected After some optimizations first transitions are calculated quickly The renaming operators help in optimizing the first transitions calculation Some models produce very many first transitions only some of which are actually solvable Such models take long to simulate because each first transition has to be looked at with the help of Mathematica For models with underspecific clauses i e where model variable behavior is not completely specified the simulator asks for more clause predicates during simulation For random simulation it is therefore useful to rewrite such models in a more specific form Architecture The design of the simulator is modular in the requested respects clause formalisms and input file formats In addition it is modular with respect to new HyPA operators the renaming operators were easy to add The architecture is such that other user interfaces and other engines can be used This has proven useful in the design of the user interface Further research There is room for further work in several respects unfulfilled r
100. p ise s v By definition of Fg p q and Fg p q and OS rule 5 we get ars d gt x t Pe A d gt 2 0 3 s v F a v OS rule 18 For some p p q v we have I a v and p v p v Furthermore we have either t p q and t p q or t q p and t q p or t p q and Y p q By induction Jaz d gt z p Fg p d gt z v gt s v Since I a v we have by OS rules 1 2 3 4 5 that x a Therefore by the definition of Fg p q and Fg p q we have das d gt x t Felt A d gt 2 0 gt s v OS rule 19 For some p p q 4 a1 a5 a v we have I a v and p v a p v and q v 3 q v and ar az a Furthermore t p q or t p q and t p q By induction and OS rule 1 2 3 4 5 we have Ja s di gt a1 p Fg p di gt aj v gt s v and 3a s do gt a2 q Fg q da gt ag v gt s v By OS rule 5 and the definition of A we get that di da gt a v gt e v Therefore by definition of Fg p q and Fg p q we have dq ld gt z t Felt A d gt 2 4 5 s v OS rule 20 For some p p a v we have a v and p v p v and t Og p and Oy p and a g H By induction and OS rules 1 2 3 4 5 Ja d gt a p Fr p d gt a v gt s v Thus by the definition of Fg Og p we have Jas d gt x t
101. p operator was introduced for calculating with process terms rather than for specification 4 1 3 2 Equality of resulting transitions F t returns a set of process term pairs This raises the question of how to determine wether two process terms are equal One problem lies in determining the equality of clauses This would probably take as much time as solving them if at all possible An efficient approximation is simplifying the clauses using some simple rules and then comparing them literally Useful rules are d Vm true gt d LT RA Loe gt VLOV pred d true 2 tr elvd gt d dvd gt d dv Vin true gt Vin true true Jr true 40 4 2 Additional HyPA operators These rules are chosen based on observations of the forms of clauses produced by Fg t The rules are sound i e the clauses on the left and right of each rule have the same solutions This follows from the definition of a solution to a reinitialization clause definition 2 3 The comparison of process terms can be enhanced by taking commutativity and associativity into account This still does not yield a complete equality function but it already eliminates many duplicate transitions 4 1 3 3 Dynamic programming Evaluating an inductive function can lead to many evaluations of the same sub term A solution is to cache results In our case Fz t likely results in multiple evaluations of F X X V It is good modeling p
102. pb qv p gt qv p K qv q v Y av 5 qv DEE CERES T Rules 11 to 14 define the semantics of the disrupt operator and the left disrupt operator If we compare these rules to the rules for sequential composition we see that the main difference is the way in which termination is handled Firstly in a composition p q the process q may start execution without p terminating Secondly if the process p terminates the process p gt q may also terminate regardless of the behavior of q Rules 15 to 19 define the semantics of the parallel composition and in these rules the difference between action transitions and flow transitions is most prominent Discrete actions that are placed in parallel are interleaved but can also synchronize using a partial commutative and 12 2 1 Syntax Table 2 4 Operational semantics of HyPA parallel composition pv Y qv Y pv gt p v au gt q v plana gt Olan Saws plav plav Ld pv gt p v 4 7 47 p v E p vl 18 Men x E S plav 5 a v qi PY S LD U av o old G MP alp v gt p v SEL t Rupe p v E p il av TE quu al 474 49 pilav gt 9 14 0 pilav SS p d v associative communication function y Ax At A If a discrete action a communicates with an action a this is the case if aya is defined the result is an action a aya If flow clauses are placed in parallel they always
103. prefix a or a flow prefix c gt A recursive specification E is guarded if for each recursive definition X p E p is derivably equal to a guarded process term using the axiomatization of HyPA This leads to the principle given in table 2 9 As an example the process terms e G a d gt X and c gt X Y are guarded while the process terms c K X and X B a X are not That unguarded recursive equations do not necessarily have a unique solution can be seen from the fact that the processes c and true are both solutions of the equation Y c Y Also the equation Z Z amp a Z has multiple solutions some of which even execute flow transitions Sadly we do not have notation in HyPA to specify these unexpected solutions From RSP it follows that the set of equations Xi OQ O d 2 Xa Xo r c gt X4 amp X3 has unique solutions for X and X Moreover it is proven that the solution of a guarded recursive specification is bounded non deterministic Definition 2 11 Bounded non determinism Bounded non determinism is recursively defined as e Every state has bounded non determinism in 0 steps e A state p v has bounded non determinism in n 1 steps if for every I the set R p v i p v Es p v is finite and all elements p v R have bounded non determinism in n steps themselves e A state p v has bounded non determinism denoted B p v if it has bounded non determi
104. r 5 Design This chapter describes the higher level design decisions made in building the simulator This includes the architecture of the system the input file format and clause formalisms 5 1 Architecture The architectural design of the simulator is described here We use the UML static structure symbols depicted in figure 5 1 Our terminology includes the design patterns defined in 8 We give a short explanation of the used design patterns Facade One single class provides the interface to a complex program part This class itself provides no functionality but is there to simplify the use of the program part Factory This pattern is used to separate the creation of subclass instances from the knowledge of which subclass to use This knowledge is within a separate Factory class An object is created by invoking a Factory class method Factory subclasses implement the creation and return objects of different subclasses Observer Used for notifying multiple observers of changes in a portion of the state the sub ject Each observer registers itself with the subject and is thereafter notified of any change in the subject Singleton Used when there may be only one instance of a class It involves hiding the constructor of the class and access to the instance is provided through a static method Access to the instance is hereby given to every part of the program that knows about the existence of the class Visitor A patte
105. ractice not to write the same term twice in a model but to use a recursion variable instead Since the set E of recursion variable definitions does not change during simulation it is very helpful to cache F X for all 0 lt n naa and X V 4 2 Additional HyPA operators Many real life models have sub processes that have a lot in common In order to be able to specify such similar processes easily we need some new operators The model variable abstraction operator defined in 18 is helpful but not enough We also define an action renaming operator pa p and a model variable renaming operator oy p Besides ease of writing of HyPA models the new operators allow for a more efficient imple mentation of the first transitions function when the first transitions for a process p are known it is relatively easy to derive the first transitions for multiple renamed versions of p 4 2 1 Action renaming The action renaming operator renames actions in transitions Its operational semantics are in table 4 1 The operator takes a map A A A and a process Whenever the process can do an action transition a v the renamed process can do the action transition A a v Table 4 1 Operational semantics of HyPA action renaming av p v Y 25 p v BaN p v palp v Y pa p v pa p v 26 Theorem 4 8 Robust bisimilation is a congruence for action renaming Robust bisimilation is a congruence for action
106. ration The simulator needs to know which clause formalism is used so there is a clause formalism declaration in every input file The consequence of these changes is that models written for the linearization tool must be extended with a clause declaration and variable declarations before they can be simulated Also extra brackets may be required to indicate the associativity of re initializations Design decision 5 23 Syntactic sugar To make writing models less cumbersome some syntactic sugar is added We mention them here and explain them in detail below e Action declarations and communication declarations can be combined into actcomm decla rations e There is an abbreviation Vm for the entire set of model variables e There is an abbreviation halves for all the halves of the communications 63 Chapter 5 Design The syntactic sugar described above makes writing models easier but the linearization tool is unable to read models that use it Below the entire file format is described Clause formalism declaration There is one clause formalism declaration and it must precede the process declarations described later Tt starts with the words clause formalism and is followed by the name of the formalism used for the clauses in the model Currently defined clause formalisms are mathematica numeri cal mathematica formalism symbolicmma symbolic mathematica formalism and clauseformalismstub for testing purposes o
107. read 1 16 F Linearized HyPA models can be simulated 1 35 F The simulator can handle equations between the derivative of a model variable and other model variables and constants 1 36 F The simulator can handle equations between model variables and con stants as flow predicates and reinitialization predicates 1 5 F The value of model variables over time can be visualized an X T plot 1 21 F It is clear at which time the discrete actions have taken place 1 30 F Initial values for the model variables can be entered by the user 1 8 F Step by step simulation is possible i e every choice is left to the user 1 9 F In step by step simulation the visualizations of the model variables are up to date when a choice or a deadlock occurs 1 34 F The choice for the time length of a flow clause can be made through vertical slide bars in the X T plots 1 51 F The default choice for the time length of a flow clause is the maximum possible time length 1 2 P By adding a class and a reference other file formats can be read 48 F Each X T plot should show the names of the visualized variables in the caption 2 49 F During a flow time choice the X T plots should show clear indications of the minimum and maximum possible time length 2 50 F In a transition choice all transitions are displayed Double clicking a transition chooses that transition and performs it 31 Chapter 3 Requirements Table 3 2 Requirements w
108. ready quite expressive Status Fulfilled ID 37 Priority 11 Description The simulator can handle inequalities in flow clauses and reinitialization clauses Motivation Inequalities can be convenient for example in the specification of the clock variable in the steam boiler model of section 7 1 Status Fulfilled ID 39 Priority 22 Description The simulator can handle all differential equations that the solver tool can handle Motivation It is useful to be able to use the knowledge that a certain mathematical solver is used Status Fulfilled 24 3 2 Requirements ID 47 Priority 25 Description The simulator can handle ordinary differential equations definition A 3 Motivation ODEs occur in existing example models in literature see section 3 2 2 1 Status Fulfilled 3 2 3 Visualization The purpose of the simulator is to visualize a trace through the state space of a given model From 20 we already know some convenient visualizations Motivation for the requirements is clear so these requirements are given in condensed form ID Prio Status Description 6 3 Fulfilled There are X T plots of variables over time 48 2 Fulfilled Each X T plot shows the names of the visualized variables in the caption 49 2 Fulfilled During a flow time choice the X T plots show clear indica tions
109. renaming Proof The OS rules of HyPA combined with the rules for action renaming are in the process tyft format of 11 Therefore stateless bisimilarity as defined in that article is a congruence for all HyPA 41 Chapter 4 Analysis operators As proven in 6 Appendix B stateless bisimilation coincides with robust bisimilation and therefore robust bisimilation is a congruence as well 4 2 2 Model variable renaming The model variable renaming operator renames variables in transitions Its operational semantics are in table 4 2 The operator takes a bijection V Vm Vm and a process This must be a bijection because all valuations in a model range over the same set V of model variables Therefore you cannot rename two variables X and Y both to X for example Below we use the following notational conventions e For a valuation v V v indicates v o V e Likewise for a flow c V c indicates o o V e For a flow clause c V c is the clause c with all variables in its jump set and predicate replaced according to V e For a reinitialization clause d V d is the clause d with all variables replaced according to V e We use notation V for the inverse of V This inverse function exists because V in ov p is required to be a bijective function Table 4 2 Operational semantics of HyPA model variable renaming pv Y pv L p i 28 29 ov p v Y ov p Viv LD oy p Vv p v p v
110. rge two valuations and two flows respectively The first function takes the valuations of the variables in the set V from v and the valuations of all other variables from u Similarly the second one takes the flows of the variables in the set V from o and the flows of all other variables from c Intuitively this works like opening a new variable scope in a procedural programming language because the newly introduced variables hide existing variables with the same name For any u v Val 0 0 X and V C Vm Jun ifngV hi Lyu Lo ifneV c n ifngV a n ifneV Furthermore v y denotes the valuation where dom v ly V and v v n v n for all n V V denotes the complement of V Finally o T denotes the valuation of the flows in o in the last element of its domain Table 4 3 Operational semantics of HyPA model variable abstraction TE mv p my u v ES pw LV pli A V w Ivy p my w u 32 p my 4 v gt p w Viv lp u M IL V wy p mv w o 1 LV v p u v LV pile v 33 34 a cs ou 35 ULV po a gt Gh w LV ev ple gt pw ULV pliu gt w 36 Rule 31 states that the abstraction of a terminating process can also terminate Rule 32 describes the case for a discrete action transition This rule expresses an essential point of the abstraction operator namely that the valuations of abstracted variables
111. ribe this set in a finite way In this section we provide a mechanism to determine the set of possible transitions that the HyPA model can perform given the current state One solution is to use the HyPA linearization tool 18 to create a Linear Recursive Specifica tion definition B 1 From such a linear specification the possible first transitions are more easily deductible than from a recursive specification in general However there are several drawbacks to this approach e Linearization is time consuming e The resulting Linear Recursive Specification can be very large e There are severe restrictions on the models that the linearization tool can handle Another approach turns out to be simple and it allows for any substitutably guarded HyPA model definition 2 12 to be simulated From the HyPA operational semantics section 2 1 1 an inductive function is derived that calculates the set of first transitions The transitions given by the operational semantics are tuples p v a v p v or p v o p v where e p v p v are states with p p process terms and v v valuations of the model variables e a v is an action label consisting of an action a and a valuation v e g is a flow 33 Chapter 4 Analysis Since the start state p v is always the current state we omit it from the results In order to keep the set of transitions finite we do not calculate the flows c and end
112. rical computation turns out to have its disadvantages so the symbolic symbolicmma formalism succeeds mathematica The following sections describe each formalism 67 Chapter 5 Design Table 5 7 Example model in input format clause formalism mathematica var waterlevel inflow act ropen sopen open rclose sclose close comm ropen sopen open rclose sclose close initial proc I encap ropen sopen rclose sclose Water Valve Controller proc Water proc Valve inflow CL inflow inflowN inflow inflowN waterlevel waterlevel t inflow t 1 inflow t 0 0 gt gt rclose Valve 3 gt gt ropen Valve proc Controller True gt ropen Controller rclose Controller 68 5 3 Clause formalisms 5 3 1 Formalism number one Formalism number one was never fully implemented and is not supported anymore by the final versions of the simulator Therefore we do not describe it in detail Its language was designed with the thought that we wanted to get something working soon and not with any practical application in mind It is a language consisting of variables functions the basic operators remainder power In log This language was then to be translated to the different mathematical solvers mathematica matlab etc A huge drawback is the difficulties this creates in representing the answers returned by the solver since the set of op
113. ription The number of steps to undo can be indicated by the user in the X T plots Motivation Status Not implemented yet 27 Chapter 3 Requirements ID 31 Priority 26 Description The simulator can be set up so that it fills in a random function for a given unconstrained model variable Motivation In a model on which analysis is performed much of the world outside of a system is left unspecified In the steam boiler example of section 7 1 for example the flow of steam is specified as a flow clause E PA In simulation you need to choose an actual behavior of the outside world This requirement is meant to lighten the burden this places on the user Status Not implemented ID 32 Priority 26 Description The simulator can be set up so that it fills in a random continuous function for a given unconstrained model variable Motivation Status Not implemented Deleted requirements ID 10 Priority 4 Description Random simulation until a stop criterium is possible Motivation Status Deleted this requirement is already contained in the newer requirements 44 and 45 ID 11 Priority 4 Description In random simulation the visualizations are updated at the end of the simulation Motivation In order to be able to simulate randomly as quick as possible it may be convenient not to update the visuali
114. rminal String action list var list var non terminal String comm section comm list comm non terminal String actcomm section actcomm list actcomm non terminal String definition section non terminal String proc non terminal HiElement proc expr non terminal TreeSet id list non terminal TreeMap rename list Precedences precedence left ALTERNATIVEOP precedence left BAR precedence left LPARALLELOP precedence left PARALLELOP precedence right REINITOP precedence left LDISRUPTOP precedence left DISRUPTOP precedence right SEQUENTIALOP 129 Chapter G Input file format grammar precedence left AND OR precedence left CONCAT precedence left CJMP SAT precedence left LSQBRACKET precedence left LPAREN The grammar Spec section s spec s1 section s2 section clauseformalism s actions_section s comm section s actcomm section s var section s definition section s proc s action list ID s action list ID s action list COMMA ID s clauseformalism actions section 3 CLAUSEFORMALISMHEADER TD 1 ACTHEADER action_list ee COMMHEADER comm list E ROA DEFHEADER LSQBRACKET PREDICATE pred a ACTCOMMHEADER actcomm list comm list comm comm list comm comm list COMMA comm comm ID si BAR ID s2 EQUALS ID s3 actcomm list actcomm actcomm list actcomm actcomm list COMMA actcomm actcomm ID si
115. rn used to traverse trees of objects Each tree node guides the visitor class to its sub nodes The visitor has a method for each type of node that it can encounter Upon reaching a node the corresponding method is invoked First we make a rough division of the system into parts Then we describe the design of each part 5 1 1 Rough division The user interface of the simulator is built first in the eXtreme Programming fashion 3 This way we know that we build what the user wants and we find out exactly what is needed underneath the user interface This calls for an architectural division of the software into two parts ui and engine 47 Chapter 5 Design Figure 5 1 Legend package Package1 Class1 class generalization inheritance WH gt association composition interface Interface2 Eg cues Interface Interface1 o implementation 5 1 Architecture Design decision 5 1 Rough division The system is divided into two parts The user interface part contains all dialogs buttons and visualizations It is responsible for coordinating all visualizations and for receiving user input The engine performs all calculations parsing determining first transitions and solving clauses This division is visible in the package structure of the program figure 5 2 Design decision 5 2 Package structure We have three top level packages ui for the ui part engine for
116. rols are in a tool bar at the top On the upper left we see the currently possible transitions The upper right section shows actions that have occurred and the plots show the continuous behavior On the lower left is a legend showing the color used for each variable and the current value of the variables 111 Chapter E Screenshots Figure E 1 Prototype 1 user interface L asprozquoj os lt lt ZOT gt m 1371013009 lt lt 86T gt gt ZOT 1377101340 98 lt lt 86T lt m STO O gt 3 V T i31 3 lt lt 0 4a 3 1211012403 uadgaaTeA o3 0 A uadosaTeA 3S0TI2ATBA 21 OT A uadgaaTe oz gt gt 0 223e2H s aA mM n 12989 2a11022u03 I 3SOTJ3ATBA UadgaaTea I 13189H aal os as oz oaj deous X 201d Teratur 3S0T9 os 91 usado os oa moo uado asora os os oz az 32e ed y 1a oq 103ejnwis mmm p a SL gt 115 PA TEL e 1 Zl DX 112 Figure E 2 Prototype 2 user interface SIO0 gt L EuLE C LS SL001Z M4 1E S S D A L SIO0 gt L Zvl 07 157 520077 M Leo s Q A L SIO0 gt L LS SA00 AW G S 0 A L lt 113 Chapter E Screenshots Figure E 3 Working version user interface LTR SaseJ UajjPPOw aneIua
117. roof would become incomplete with each addition of a new axiom Since any axiom has to satisfy robust bisimilarity we could try to relate a structural property to a property of the underlying transition system However this approach has not been successful so far 4 1 2 2 Fixpoint approach A solution for termination of Fg t could be to try and find a fixpoint Suppose we have a mapping m of recursion variables to sets of first transitions We replace rule 14 of Fg t by F X m X Repeatedly we calculate m X m X U F rhs X for each recursion variable X Y until m does not change If we can prove that such a fixpoint exists and that it is reached then we have a first transitions function that is well defined This approach is not practical as we describe next We begin with some notational conven tions from 4 Partial order We denote a partial order by D E Here D is a set and C is a reflexive anti symmetric and transitive relation on D x D A partial order is complete if 1 it has a least element 1 such that Vae pL E d and 2 every chain see below has a least upper bound see below Chain Let D GC be a partial order A chain with respect to D E is an infinite sequence of elements do di such that do E d E We denote such a chain by di i gt 0 Least upper bound An upper bound of a chain d gt o is an element d such that Visod E dn For a least upper bound we al
118. rted by priority is given 3 1 Overview The simulator takes a HyPA model and visualizes a trace of transitions that the model can perform Since a HyPA model typically has many different possible traces choices must be made at certain points in the simulation The simulator is to have two modes of operation step wise simulation in which the user makes the choices and random simulation in which the simulator makes the choices The visualizations should give a clear impression of the continuous and discrete behavior of the model The simulator should be easily extensible in some respects For example the architecture of the simulator should be such that other input file formats and other clause formalisms can be added easily 3 2 Requirements Each requirement is described by the following fields ID A unique number for the requirement for easy reference Priority The importance of the requirement a lower number means a higher importance Description A description of the requirement Motivation Why the requirement is present Status The extent to which the requirement is fulfilled 3 2 1 HyPA input It is hard if not impossible to implement a simulator for all possible HyPA models The re quirements presented here indicate which classes of models should be handled correctly by the simulator First of all there is the HyPAyn class used by the linearization tool Along the lines of e g pCRL we also define a class of models calle
119. sed turned out to be cumbersome to implement and to be restrictive to the user The mathematica related formalisms allow the use of most Mathematica constructs that are available They fulfill all requirements about classes of differential equations to be handled Numeric calculation does have its limitations forced ending of a flow is not always calculated correctly and the precision and accuracy of the calculation is not really controllable The latter is a property of Mathematica Because of this models often need to be rewritten to let them behave as desired under numeric calculation Symbolic calculation can be used for a more limited class of differential equations than in the numeric case but it works as expected Models written for analysis purposes do not have to be rewritten Cimp COnstructs turn out to be difficult to solve This is mainly a problem of Mathematica Therefore the currently implemented clause formalisms do not implement Cjmp solving The sim ulator do es allow for HyPA models with c to be read and the design is such that cj solving formalisms can easily be added The first transitions function introduces Cjmp constructs for cer tain HyPA models The simulator rewrites models such that that does not occur The rewrite process is proven to produce robustly bisimilar models This could not be achieved by using the HyPA derivation system but had to be done using witnessing relations The HyPA derivation system turns
120. shing requirements number 1 through 22 section 3 prototypes of the user interface are produced Screenshots of these prototypes can be found in Figures E 1 and E 2 The prototypes show the different visualizations of model behavior and indicate the way in which the simulator will be controlled by the user Evaluation of the pro totypes leads to requirements 23 through 47 After two user interface prototypes a new iteration is started which produces a first simulator version Successive iterations provide simulators that implement more and more of the requirements 1 4 Structure of this thesis Chapter 2 gives an introduction to the HyPA language After that the phases of the development process requirements analysis all have their own chapter Finally conclusions are presented in chapter 8 Chapter 2 HyPA semantics and axioms This chapter gives an introduction to HyPA It is a slightly compressed copy of 6 chapter 3 First the syntax is described followed by the semantics and axioms The HyPA axioms have been rearranged and numbered for ease of reference in the rest of this document Finally definition 2 12 is taken from 18 19 2 1 Syntax The signature of HyPA consists of the following constant and function symbols 1 deadlock 2 empty process e 3 discrete actions a A 4 flow clauses c C 5 a family of process re initialization operators d gt gc p 6 alternative composition _
121. so have that for any other upper bound dm dn C dm When it exists we denote the least upper bound by U gt od Now we give some definitions of our own and try to prove that the fixpoint approach works This fails and we explain why Definition 4 3 First transitions set We introduce a notation amp for the type of first transitions A first transition is a pair p p Term p describes the transition and is of the form d gt or d gt a or d gt c Term p describes the resulting state after performing the transition In case of termination p Y Definition 4 4 First transitions mapping Define M as abbreviation for the type V P 3 i e a mapping of recursion variables to sets of first transitions Definition 4 5 C 37 Chapter 4 Analysis Let m m M Now define the relation C on M x M as follows m E m iff Vxey m X m X Lemma 4 1 P M C is a CPO P M C is a complete partial order Proof Trivially P M C is reflexive anti symmetric and transitive Therefore it is a partial order gt Furthermore it has a least element Y X 1 X V Finally every chain s gt o has a least upper bound given by X Uso s X X Vi Definition 4 6 F7 t Let m be a first transitions mapping Redefine the first transitions function Fg t to F t by replacing rule 14 with F X m X and replacing every occurrence of Fg p by FR p
122. st be a global variable for each abstracted variable Thus the abstraction operator abstracts from variable behavior not from the variables themselves We would like to be able to simulate all models that can be linearized i e HyPAji models appendix B These models can have one occurrence of an abstraction operator namely at the 45 Chapter 4 Analysis top level This means that the behavior of some variables is hidden During simulation the be havior of all variables global and abstracted needs to be specified This means that the simulator must bother the user about initial values and behavior for abstracted variables anyway To avoid bothering the user about the redundant global variables as well we can implement abstraction for HyPA rin models simply by erasing it from the model We do not implement full support for the abstraction operator for a number of reasons 1 The user needs to give initial values for all variables including abstract ones This means that for simulation abstraction does not really work Variables can already be removed from the graphical representations of the behavior It is unlikely that the abstraction operator will be used in models since the linearization tool does not support it fully Next to the new renaming operators abstraction is not needed to simplify writing of models Considering the drawbacks and usability it is a lot of work to implement abstraction 46 Chapte
123. st we prove that the induction is well defined and then that it actually gives the first transitions C 1 F t is well defined for substitutably guarded models Definition C 1 Weight function For a substitutably guarded specification t E define the weight of t E notation w t E as a pair 5 0 where e sis the number of substitutions needed to make t completely guarded and e o is the number of operators in t Since t is finite and t E is guarded w t E is finite Theorem C 1 Well definedness Fg t is well defined for substututably guarded specifications Proof The weight of specifications in the right hand side of all rules in the definition for Fr t decreases with respect to the lexicographic order Rules 1 through 4 w t E 0 0 and Fr does not occur in the right hand side Rules 5 6 8 10 through 13 the number of operators in p and q is one less than in t and no guarded recursion variables become unguarded so if w t E s o then w p E w g E 5 0 1 Rule 7 the number of operators in p and q is one less than in t However possibly a guarded recursion variable becomes unguarded This can only be the case when p a for some action a This implies however that Fg p true gt a e and thus Fg q is never evaluated Rule 9 Only Fr p is evaluated in Fg p gt q which decreases the number of operators as well as the number of possibly unguarded recursion variables
124. step by step sim ulation in which the simulator stops whenever there is a choice to make The user chooses a next transition and performs it then chooses the next transition and so on The other mode of simulation is random in which the simulator makes each choice in a random way until some stop 25 Chapter 3 Requirements criterium is reached Upon meeting the stop criterium simulation resumes in step by step mode ID 30 Priority 1 Description Initial values for the model variables can be entered by the user Motivation The initial value for model variables is often left unspecified in models In a simulation initial values must be chosen Status Fulfilled ID 8 Priority 1 Description Step by step simulation is possible i e every choice is left to the user Motivation Status Fulfilled ID 9 Priority 1 Description In step by step simulation the visualizations of the model variables are up to date when a choice or a deadlock occurs Motivation Status Fulfilled ID 34 Priority 1 Description The choice for the time length of a flow clause can be made through slide bars in the X T plots Motivation This method designed by Huub van den Broek 20 has proven to be convenient Status Fulfilled ID 51 Priority 1 Description The default choice for the time length of a flow clause is the
125. step wise simulation you are presented with a choice after each transition The simulator finds out which transitions the model can do and displays them in the choice box Also it tries to solve the clauses in these transitions for a while The time that the simulator spends on solving is a setting section F 8 The solutions are also shown in the choice box Figure F 3 shows two transitions that each have one solution The transitions are preceded by a grey white dot and the solutions by a green one The first transition in the figure is an action transition the second one a flow transition Figure F 3 Choice box Possible transitions on dl temperature 0 Ym temperature t K 30 temperature t amp amp temperature lt Tmax t 0 10 00 numerical solution gt In section 4 1 1 it is explained that first transitions are of the form d gt a d gt cor d gt e The simulator initially only shows the a c or e Also there is a set of next processes per transition For each next process a separate transition is shown in the choice box You can right click on the choice box to show the reinitialization and the next processes F 5 1 Solving transitions If a transition is not solved due to the time limit it is shown without solutions You can select such a transition and press button 4 to solve it manually Alternatively you can press button 5 118 F 6 Random simulation to solve all transitions F
126. sym ID yytext lt CLAUSEBEGIN gt gn return symbol HyPA ASCII sym COMMA T Identifier return symbol HyPA ASCII sym ID yytext yybegin CLAUSEPRED predicate bracketCount 1 return symbol HyPA_ASCII_sym BAR WhiteSpace Ignore Comment T Ignore lt CLAUSEPRED gt ME bracketCount predicate Predicate predicate yytextO bracketCount if bracketCount 0 yybegin YYINITIAL return symbol HyPA ASCII sym PREDICATE predicate else predicate lt DEFINITIONBEGIN gt 127 Chapter G Input file format grammar yybegin DEFINITIONPRED predicate bracketCount 1 return symbol HyPA_ASCII_sym LSQBRACKET WhiteSpace Ignore Comment Ignore T lt DEFINITIONPRED gt os bracketCount predicate Predicate predicate yytextO bracketCount if bracketCount 0 yybegin YYINITIAL return symbol HyPA ASCII sym PREDICATE predicate gt else predicate error fallback An throw new EHSParseException Illegal character X yytext MX encountered at line yyline 1 column yycolumn 1 G 2 JavaCUP input The following grammar leads JavaCUP to produce a parser for HyPA Input file for the CUP parser generator Parser definition for the HyPASim input file format number
127. synchronize their behavior such that intuitively the flows that are possible in a parallel composition are a solution of both clauses Encapsulation as defined by rules 20 to 22 only influences action transitions This is not surprising since as mentioned before the Oy _ operator is originally intended to model enforced synchronization in a parallel composition Parallel composition in general may lead to interleaving actions and synchronized actions The encapsulation operator is then used to block the interleaving actions Flow transitions are already synchronized in the parallel composition so there is no need for encapsulation of those Table 2 5 Operational semantics of HyPA encapsulation and recursion U a V pv gt p v ag H 20 On p v gt On p v pv v 21 p v Y 29 On p v On P v On p v V QUY QU 4 v TUA X peE P ie 24 X pe E Rules 23 and 24 model recursion For a recursive definition X p a transition for the variable X is possible if it can be deduced from the semantical rules for the process term p 13 Chapter 2 HyPA semantics and axioms 2 2 Algebraic reasoning in HyPA The strength of the field of process algebra lies in its ability to use equational reasoning for the analysis of transition systems or more precisely for the analysis of equivalence classes of transition systems called processes In this section we show that
128. t ilt Vm clock t 21 ig 0 A vj v gt DiodeOn DiodeOff gt Diode Vn iot 20 i t i2 t vilt valt Ya v t v t dolt t i2 t iolt 20 Ya volt v t io t Ro Ya vt i2 t R Vin v t sin 27 felock t 84 7 6 Half wave rectifier Figure 7 6 Half wave rectifier voltages 85 Chapter 7 Cases Figure 7 7 Half wave rectifier currents 86 7 6 Half wave rectifier A 1 Table 7 7 Vm clock i0 il i2 vO v1 v2 f 10 R0 10 R1 30 C0 50 x 107 e 0 001 Rectifier SystemOff SystemOn System CapacitorO Clock DiodeOff DiodeOn Resistor0 Resistorl Source Switch SystemOn SystemOff System DiodeOff gt Switch System DiodeOn gt Switch Clock Source Resistor0 Capacitor0 Resistor1 Vm Cov2 t t clock clock t 21 io i2 va ig lt 0 eAo 2v enig U AT 0 6 gt SystemOn amp do i2 va ig lt 0 eno vg Heij OAif OA it io t 20 i t i2 t vi v e v t valt A dolt i t i2 t io gt 0 e volt vilt ig t Ro valt io t Ri volt sin 27 felock t gt SystemOff 87 0Av v 0Av v Chapter 7 Cases 88 Chapter 8 Conclusions The goal of this thesis was to build a simulator for HyPA It should be
129. t Also it hides the complexity of the actual engine implementation Design decision 5 7 Abstract Engine class There is a Fagade to the engine that consists of an abstract class named Engine Subclasses DummyEngine and RealEngine then implement the different engines figure 5 8 The class has the methods listed in table 5 2 More detailed specifications of the methods can be found in the implementation documentation There are restrictions to the order in which the methods may be called These correspond to the user command restrictions of figure 5 5 First a specification must be loaded Then all other methods may be called Initial values may only be set before performing any transitions Transi tions may only be undone after performing them Design decision 5 8 Singleton Engine class In order to make the current Engine instance available to the many classes of the ui package we use the Singleton design pattern 8 The abstract class Engine has an initialize method that takes a subclass instance This method is to be called once After that a public static method instance provides access to the sole instance Table 5 2 Engine methods loadSpecification filename Loads a HyPA specification from a given file getSpecification Text Returns the original specification text getSpecification Returns the specification as an object getModelVariables Returns a list of all model variables get Current Time Returns the sum of
130. t 1 gt a1 a Using bisimilarity we find that X Y since the value of x is set to 1 by the first action a1 the second re initialization of X is irrelevant However placing these processes in parallel with the process Z Ea rt 2 gt as clearly shows a difference One might expect that X Z Y Z but the sharing of variables leads to the result that the sequence a followed by az gives a deadlock situation for X Z while the action az can still occur for Y Z The interference of Z shows a difference between X and Ye In order for the equivalence to be robust with respect to interference caused by processes executed in parallel for all states that are reached by performing transitions it is required that the contained process terms are related for all valuations that can be obtained through interference This is what we call robustness of a relation An interference can be modeled as a function ut Val Val Observe that we apply the same interference function to both variable valuations Definition 2 6 Robust A relation R C T V x Val x T V x Val is robust if for all p v p v X such that p v R p v and for all interferences y Val Val we find p v R p v v Definition 2 7 Robust bisimilarity Two process terms p q 7 Y are robustly bisimilar denoted p q if there exists a robust bisimulation relation R C 7 V x Val x 7 V x Val such that p v R q
131. t random simulation Start random simulation until a stop criterium is reached Add an X T plot Add an X Y plot Add an X T plot for each model variable Remove one or more plots Fit all plot axis ranges so that everything is visible Settings for auto adjustment of plots during simulation 117 Chapter F User manual F 4 Loading a HyPA model To load a HyPA model press button 1 You are presented with a file chooser dialog The simulator assumes that HyPA model files have extension hypa Choose a file and click OK Now several things happen e Dependent on the clause formalism used in the model Mathematica is started visible in the Windows task bar e One X T plot is shown that has all the model variables in it e The legend shows all model variables in the model e The simulator starts solving the transitions that the model can do It will do this until all first transitions are solved or until a timeout expires see below F 8 You can view the model file contents on the Specification tab above the action viewer In ternally the simulator uses a rewritten version of the model see section 4 1 3 1 This rewritten version is under the Rewritten spec tab Because no transitions have been performed yet you have the option of setting initial values for the model variables You can do so by pressing button 2 How the initial values should be entered is clause formalism specific F 5 Step wise simulation In
132. takes care of formatting 6 3 Parsing The well known combination of JFLEX and JavaCUP is used to generate the various parsers needed by the simulator Separate parsers are used for the HyPA language and per clause formalism for reinitialization and for flow clauses The grammars for the input languages can be found in appendix G 6 4 Plotting Inspired by the simulators CHARON and HyVisual we started out by using the Ptolemy Plot library 13 for plotting continuous behavior Extending these classes proved difficult and we designed our own plot classes specifically for this solver see also section 5 1 2 1 73 Chapter 6 Implementation 74 Chapter 7 Cases This chapter lists the more interesting HyPA models used in case studies Many smaller test models are not listed in this document All models described here are simulated using the symbolic mathematica clause formalism althogh for most models numeric versions were also constructed For readability and for consitency throughout this document all models are not given in the input file format but in standard HyPA format 7 1 Steam boiler The model in table 7 1 is the steam boiler example from 7 section 2 4 There is a container of water The water level must be kept between a minimum and maximum level Water continuously evaporates from the container A controller has the ability to open or close a valve which releases water into the container The controller looks
133. te ig O A vy v by something like jig lt 0 001 A v v lt 0 001 This creates a problem with the flow clause for DiodeOff unless ig is exactly zero the equation io t 0 cannot be satisfied without a jump at the start of the flow A solution to this is to extend the reinitialization with ij 0 A vj vg This ensures that io is zero and that v equals va after the reinitialization But it creates difficulties with the other differential equations some variables have jumped and some have not creating a discrepancy Now the only solution is to let the other variables jump as well in such a fashion that all equations are satisfied at the beginning of the next flow This means that knowledge about the whole system is now incorporated in the reinitialization for the diode Even after rewriting the model in this fashion table 7 7 it cannot be simulated the math ematica NMinimize function cannot handle inequalities on the sine wave This implies that the flows do not end when they should so that the diode does not switch modes in time The sine wave remains un simulated 83 Chapter 7 Cases Figure 7 5 Half wave rectifier figure taken from 17 Table 7 6 Rectifier Van 1 clock 10 11 19 Vo U1 va f 1 Ro 10 Ry 30 Co 50 x 1073 Rectifier Capacitor0 Clock Diode DiodeOff DiodeOn Resistor0 Resistor 1 Source Clock Source Resistor0 Capacitor0 Resistor1 Diode Ya Covg
134. tes Reinitialization predicates are combinations of equalities and inequalities over the previous and next value of the model variables e Equations and inequalities are combined using amp amp The symbol is used to specify an equality The symbols lt gt lt gt can be used to specify inequalities e A previous value is indicated by the name of the model variable followed by the letter P and a next value is indicated by the name of the model variable followed by the letter N All model variable occurrences must have suffix P or N e The predicates False and True may be used Example xP 5 amp amp xN xP 10 Be cautious with equalities in reinitialization predicates Due to the errors that occur in nu meric calculation variables most likely do not reach a specified exact value For example the process term a x t 1 amp amp x 4 gt xP 4 gt e will most likely not terminate successfully A solution to this problem could be to interpret a b as a b e for some user specified constant e However this interpretation incurs its own problems Suppose there are previous as well as next values in an equation e g aP aN This new interpretation leads to many possible solutions for the reinitialization clause Another problem with the approach are constructs of the form xP 0 mes x t 0 If xP 0 is interpreted as x lt e then a solution for the flow clause is
135. that represent the different HyPA elements i e operators atomic elements clauses etc The abstract HyPAElement class has subclasses for each HyPA element to be represented Figure 5 10 depicts the class hierarchy for HyPA elements There is a subclass for each atomic HyPA element 6 e a X Then there are abstract sub classes HEUnaryOperator and HEBinaryOperator from which classes for all unary and binary oper ators are derived Since clauses can consist of atomic clauses and clause operators they have their own hierarchies e g there is an abstract class HEReinitializationClause which has subclasses HERClause atomic clause HERUnaryOperator from which is derived HERBinaryOperator for and V and and HERJump cjmp Design decision 5 12 Recursive functions Recursive functions on process terms like generating possible first transitions and creating a string representation are distributed over the HyPA element classes Design decision 5 13 Visitors Other operations on process terms can be implemented using so called Visitors 8 An abstract class HyPAVisitor is defined that is capable of traversing a process term tree Subclasses im plement some behavior on encountering the different elements An example of a visitor is the HyPAActionChecker for checking the validity of action names in a term 57 Chapter 5 Design Figure 5 10 HyPA specification object hierarchy HEFlowClause HyPASpecificati
136. the blue word TERMINATION is shown in the action viewer F 7 2 Plots There are currently two types of plots variables versus time X T and two variables versus one another X Y You can add and remove plots at any time during the simulation One can add plots by clicking button 11 add X T plot button 12 add X Y plot or button 13 add X T plot for each variable In the first two cases you are presented with a dialog to choose variables Removing plots is done using button 14 You can select one or more plots to remove in the dialog that opens F 7 2 1 X T plots An X T plot figure F 6 shows the value of one or more variables against time The variables are mentioned in the plot title at the top The blue bar at the right is the time selection bar that is mentioned in section F 5 2 You can drag it left and right to select the length of a flow transition A label now detail view in figure F 7 shows the current time Anything to the left of now is from performed transitions and anything to the right is a transition that is currently selected in the choice box 120 F 7 Visualizations Figure F 7 X T plot current time o Figure F 8 X Y plot 121 Chapter F User manual F 7 2 2 X Y plots An X Y plot figure F 8 shows the value of two variables versus one another The initial values are represented by a red dot and the last values are represented by a black dot
137. this is a single flow clause that defines a relation between voltages and currents in the system For the diode we introduce two modes of operation off and on We introduce a Clock process that models time so that we can produce the sine wave using the formula vo t sin 27 f clock t In this model there is no clear division of the model variables over the different processes For example to which process does variable y belong Current ip is influenced by Ro as well as by diode D Therefore which variables should be in the jump sets of the different flow clauses Luckily all variables in this circuit can be modeled as continuous ones so that Y4 may be put into all of the jump sets Simulating the model turns out to be a challenge The symbolic clause formalism turns out not to be able to handle the equations clock 0 0 clock t 2 1 vo 0 20 v t sin 27 f clock t The mathematica DSolve function simply does not accept them We replace the sine waveform by a saw tooth waveform using the process Source Vm v t 21 A vol 1 gt v 1 gt Val v t 1 A w t gt 1 gt vy 1 gt Source The resulting model can be simulated and the resulting voltages and currents can be found in figures 7 6 and 7 7 To simulate the sine wave numeric calculation must be tried This requires some rewriting of the model as the reinitialization predicate contains equalities We would like to replace the predica
138. tion of processes p and q The process q is executed after successful termination of the process p We use the notations and for alternative and sequential composition rather than the usual and to avoid confusion with the notation used frequently in the description of flow and re initialization predicates for addition and multiplication We realize that this might distract people in the field of process algebra yet chose to adapt the process algebraic notation rather than the notation adopted from system theory simply because the latter has been in use for a longer time already Overloading the operators is also an option since it is always clear from the context whether for example addition or choice is intended When studying HyPA as a new process algebra as is done in this thesis overloading is probably to be preferred indeed as it hardly hampers the search for process algebraic properties However when studying hybrid models in HyPA and performing analysis using axioms from both process algebra and system theory in the same proofs the overloading becomes more of a burden Furthermore when presenting these models to other hybrid researchers who are often not familiar with process algebra at all this effect is even stronger Disrupt The disrupt p gt q models a kind of sequential composition where the process q may take over execution from process p at any moment without waiting for its termination This composition is invalu
139. tion predicates while taking into account the influence of the variable set V 10 2 1 Syntax A flow clause V Pf changes the valuation of the model variables according to the possible solutions of its flow predicate Pr An initial jump in the value of a variable x is allowed in HyPA when x g V Furthermore discontinuous and non differentiable flows of x may be allowed if such solutions exists for the type of flow predicate that is used The concept of solution of a flow clause is lifted from the notion of solutions of its flow predicate as follows Definition 2 2 Solution of a flow clause A pair v c Val x F is defined to be a solution of a flow clause c C denoted v 0 c as follows e v c E V Pr if o He Pe and for all x V we find v x 0 x e v c cnd if 1 0 Ec and 1 0 E c Clearly the flow clause false has no solutions as the flow predicate false has no solutions A re initialization clause V P changes the valuation of the model variables according to the possible solutions of its re initialization predicate P The set V indicates the variables that are allowed to change their value Whenever x V the variable x is fixed Note that this is precisely opposite to the use of V in flow clauses We define the solutions of a re initialization clause in terms of the solutions of a re initialization predicate as follows Definition 2 3 Solution of a re initialization cl
140. trictly guarded models by using axioms The first transitions function is defined using the structure of the process term Also termination of the function is proven using the structure of the term Therefore we need some structural property that remains constant under axiomatic rewriting This property should ensure that the function terminates Definition 4 2 protected The occurrence of a recursion variable is protected iff it is in the scope of either t or t or t gt _ Here t must be such that not t v v for any v even if the clauses in t are satisfiable t can be any term 36 4 1 First transitions The closest we have gotten to a property that remains constant is something that we call pro tectedness definition 4 2 Note that strict guardedness guardedness without axiomatic rewriting implies protectedness It appears to remain constant under all the current axioms except for the ones concerning deadlock For example axiom 9 2 states that false gt 10 If we fill in a recursion variable for x then the left process term is not protected while the right process term is This is a problem because it implies that the first transitions function does not terminate for all guarded process terms Another problem with this approach is that new axioms may be added since the HyPA derivation system is still incomplete If we would actually prove the invariance of a certain property under the axioms this p
141. ty we can skip the termination cases since none of the given processes can terminate For the other cases any transition is a flow transition Lemmas D 1 and D 2 prove these cases Lemma D 1 pRq and p v y v implies 3j q v q v and p Rq We have three cases In all cases p c by definition of R and p c by the operational semantics Case 1 q co Trivial 109 Chapter D Rewriting flows Case 2 q C P Co By OS rule 14 we get q v Co v By definition of R we also have p Rq Case 3 q d gt Cy gt Co By OS rule 5 and the definition of the solution of a flow clause we have v o Ef c and Vrey u x o 0 x This gives us v c 0 Er d and 0 0 0 Ey Cy By OS rules 3 5 and 12 we get av c gt Ga UT By definition of R p Rq Lemma D 2 pRq and q v gt q v implies dy p v p v and p Rq We have three cases In all cases p c by definition of R and p c by the operational semantics Case 1 q c Trivial Case 2 q C gt Co We have two cases the transition from q v can be according to OS rule 12 or to OS rule 14 Case 2 1 OS rule 12 c v id q v By OS rule 5 we have that q c and thus g c P co and v o HF cy Therefore o Ef pred and Yrev v x c 0 z Since V Vm we also have V cv v x 0 0 1 and thus v c E co Thus p v p v je By definition of R p Rq Case 2 2 OS rule
142. ubject o 5 1 2 1 Visualizations The different visual controls such as X T plots X Y plots the legend the transition choice box etc require different sets of information about the current state and state changes Design decision 5 4 Use of observer pattern In order to keep the design extensible and simple we use the Observer pattern 8 to couple the controls to the visualization manager The controls depending on what information they need implement one or more of the interfaces in table 5 1 Each control is registered with the visualization manager for the information that it needs After registering it is notified of new information In the prototypes we used a freely available library to create plots However extending these plots with time choice bars proved difficult so we implemented our own plots The class hierarchy 50 5 1 Architecture is in figure 5 4 A basic Plot class contains all code common to X T and X Y plots Then the classes XTPlot and XYPlot implement the drawing of data on the plot The TimeChoiceXTPlot class adds time choice bars The XTPlot class is never used in practice because we want time choice bars on all X T plots The reason for this extra class is simply to make the code more readable the functionality is divided over more classes Table 5 1 Observer interfaces ISpecificationOberver Loading and closing of specifications IEnableObserver Enabling and disabling of possible user
143. uction Jq 4 d gt x p Fg p d gt zv s v By the form of Fg t and OS rules 1 through 5 we have that x c for some flow clause c By OS rules 3 5 and the extra assumption we have that V d gt c V v VO s V v Therefore by definition of Fr ov p we have Jar d gt x t Felt A d gt 2 0 3 s v 108 Appendix D Rewriting flows In section 4 1 3 1 Cjmp constructs are eliminated by rewriting flows This appendix gives the proof of V pred 2 X where X WWW true gt Vin pred gt X Abbreviations We introduce the following abbreviations Co for V pred Cy for Vin pred dy for Vin V true Proof outline We prove that X co is a solution for X dj gt c gt X Trivially X X is a solution as well Because d gt cy gt X is guarded we may apply the Recursive Specification Principle and we get Co y X By the soundness of we get that c r X Proof X c is a solution For this we must prove that c r dy gt cy D Co Interestingly this cannot be proven using the HyPA derivation rules Therefore we prove this by giving a witnessing robust bisimilation relation R Voc Val V CV predePrl co v R co v co v R c gt cov co v R du gt Cy D gt Co v Proof R is a robust bisimilation relation Now we prove that R is indeed a robust bisimilation relation R is robust by construction As for bisimilari
144. utably guarded This corresponds with the claim about in 2 Note 2 3 9 and with the PNUDG principle of 16 Lemma 3 6 4 4 1 3 Optimizations The first transitions function as it is presented above turns out to take too much time to calculate Also solutions to Cjmp clauses are hard to calculate There are several optimizations possible to make Fp t faster and to prevent occurrences of Cjmp 4 1 3 1 Eliminating Cjmp The first transitions function introduces Cjmp constructs in rules 10 and 12 p q and p q It turns out that a Cjmp is difficult to solve One needs to obtain all solutions to the flow clause The Mathematica NDSolve function however requires that the initial values are known already to obtain only a single solution There is a frequently occurring case in which these jumps can be eliminated if no variables are allowed to jump in the flow clauses then di Cijmp do Cajmp equals di da 6 page 75 last paragraph Fortunately any flow clause can be rewritten to a flow clause without jumps as shown in theorem 4 7 Theorem 4 7 Eliminating jumps from flow clauses The flow clause V pred is robustly bisimilar to X where X Vm V true gt Ya pred X Proof See appendix D The simulator does this transformation automatically It does not solve Cjmp so it requires that there is no actual occurrence of cjmp in the HyPA model This is not a very severe restric tion because the Cjm
145. v for all valuations v Val Robust bisimilarity is selected as the core equivalence between hybrid processes 2 2 2 Axiomatization In this subsection we give the axiomatization of robust bisimilarity in HyPA In table 2 6 we give a set of derivation rules and throughout this subsection we give a set of axioms that to a large extend capture the notion of robust bisimilarity We write HyPA Fg p r q if we can derive equivalence of p and q using those axioms and recursive definitions from a set E Definition 2 8 Derivation Let E be a set of recursive definitions over a set of recursion variables V We write HyPA Fg p amp q to indicate that equivalence of open terms p and q can be derived from our axiom system and the recursive definitions from E In cases where there can be no confusion as to the set of recursive definitions that is intended we write instead of Hg We define that equivalence can be derived according to the rules given in table 2 6 In this table p pi q qi r denote process terms d d denote re initialization clauses and c c c denote flow clauses Rules 1 2 and 3 of table 2 6 express that is an equivalence Rules 4 and 5 express that it is a congruence Rules 6 and 7 express that equivalence of flow predicates and re initialization predicates transfers to equivalence of flow clauses and re initialization clauses respectively Rule 8 expresses that a recursive specification X p gi
146. valuations v We do provide the clauses that need to be solved to obtain the flows and valuations This way we allow the user to choose a transition first before solving the clauses 4 1 1 First transitions function Our function named Fz t calculates for a substitutably guarded definition 2 12 HyPA spec ification t E the set of transitions that can be performed provided that their clauses can be solved The transitions are denoted by tuples p p Process p indicates the clauses that need to be solved and the type of transition It has one of the forms da dc de Process p is the process term of the resulting state p v In case of termination the resulting state is denoted by v In the following definition each line except for the first one can easily be traced back to a rule in the operational semantics 34 4 1 First transitions Definition 4 1 Fz t Let a A cE C de D X EV p p q q q T V and t E a substitutably guarded recursive specification Note that p p p q q q cannot be equal to V since this is not a process Define the first transitions of t E notation Fr t inductively as follows 1 Fx 0 0 2 Fz e true gt ev 3 Fila true gt a 4 Felc true gt c c 5 Fr d gt p dee ev i e ev e Fz p U d e gt p p temrp tcFz n 6 Fr p amp a Fz p U Fela 7 FE pO 4 if 3u d gt e v Fz p then
147. ves rise to an equivalence of X and p In the remainder of this subsection the axioms of HyPA and the insight they provide regarding the operators of the language are presented Rule 9 expresses that these axioms 15 Chapter 2 HyPA semantics and axioms indeed define equivalences In each of the axioms x y z denote arbitrary terms The letters a a denote actions while c c denote flow clauses and d d denote re initialization clauses One may not choose when a is written in an axiom At the end of this subsection the intuitions behind derivation rules 10 and 11 are discussed Table 2 6 Derivation rules of HyPA HyPA TE Pr q 2 HyPA Fg pz H HyPA Eg q 7 D HyPA Fg pz q HyPAbg q T HyPA Fe pz T 3 HyPA Fre pe q S Vp gt T Vj dom S NV 0 HyPA tg S p r S q 4 Oan n ary HyPA operator Vi lt i lt n HyPA Eg pi amp qi HyPA Fe O p1 Pn Zr O Qq1 qn Vo vv H d iff v v d 6 Vue 4 0 E c iff 1 0 Ed 5 HyPA Cr d gt rx d gt a HyPA Fg cz C X pcE pr q is an axiom HyPA Fg X p HyPA Fg p 7 q Ve 5 0 E C implies v o c Vivo v v E d and 1 0 H c imply 1 0 Fe HyPA egd gt c d gt c gt c Vue 1 0 E c iff 1 0 Ec or 1 0 Fe HyPA Fg ce C 6c gt ec The axioms of HyPA are presented in the tables 2 7 and 2 8 They were taken from 6 but rearranged and numbered for easy reference
148. wajduur E aren U343PN35 2 Duna q AWL Z69Sps sbunzas pue sjuauin20Q 114 Appendix F User manual This chapter describes the installation and use of the HyPA simulator F 1 Installation The following is needed in order to run the HyPA simulator e A computer running Windows XP e Mathematica version 5 1 e The Java Runtime Environment JRE version 1 4 2 or later e File hypasim jar e File hypasimW exe e File hypasim exe optional e File JLinkNativeLibrary dll The JRE can be downloaded free at http java com The file JLinkNativeLibrary dll must be placed in the jre bin directory The other two files must be in a directory together F 2 Running Running the simulator simply amounts to running hypasimW exe If the simulator does not seem to be working you might want to run hypasim exe without a W from a console DOS box That way you can see any Java specific errors that might occur There is a setting that needs to be adjusted before any models can be simulated This set ting can be found in the Tools menu under Options You are presented with a dialog with three tabs Choose the Mathematica tab In the field on that tab enter the path to the mathematica kernel Usually you can leave the default value of C Program Files Wolfram Research Mathematica V5 1MMathKernel exe F 3 User interface Figure F 1 shows the HyPAsim user interface Five main components
149. xthrow EHSParseException t int bracketCount 0 String predicate private Symbol symbol int type 1 return new Symbol type yyline 1 yycolumn 1 125 Chapter G Input file format grammar private Symbol symbol int type Object value return new Symbol type yyline 1 yycolumn 1 value ht LineTerminator r n r n InputCharacter r n WhiteSpace LineTerminator t f Comment A4 InputCharacter LineTerminator Identifier jletterdigit Predicate x5B x5D Astate CLAUSEBEGIN Astate CLAUSEPRED Astate DEFINITIONBEGIN Astate DEFINITIONPRED hh lt YYINITIAL gt headers clause formalism return symbol HyPA_ASCII_sym CLAUSEFORMALISMHEADER T act return symbol HyPA_ASCII_sym ACTHEADER T comm return symbol HyPA_ASCII_sym COMMHEADER var return symbol HyPA_ASCII_sym VARHEADER T def yybegin DEFINITIONBEGIN return symbol HyPA_ASCII_sym DEFHEADER T proc return symbol HyPA_ASCII_sym PROCHEADER initial return symbol HyPA_ASCII_sym INITIALHEADER T actcomm return symbol HyPA ASCII sym ACTCOMMHEADER T constants delta epsilon return symbol HyPA ASCII sym DELTA return symbol HyPA ASCII sym EPSILON comments and whitespace WhiteSpace 1 Ignore Comment T 1 Ignore separators U n u JE n ny return symbol H
150. yPA ASCII sym COMMA T return symbol HyPA ASCII sym LABSTRACT return symbol HyPA_ASCII_sym RABSTRACT return symbol HyPA_ASCII_sym BAR T return symbol HyPA_ASCII_sym LPAREN return symbol HyPA_ASCII_sym RPAREN T yybegin CLAUSEBEGIN return symbol HyPA_ASCII_sym LSQBRACKET T return symbol HyPA_ASCII_sym LBRACE return symbol HyPA_ASCII_sym RBRACE return symbol HyPA_ASCII_sym EQUALS T return symbol HyPA_ASCII_sym RIGHTARROW T return symbol HyPA_ASCII_sym LEFTRIGHTARROW gt lt gt a ha Cha Cha ha Cha ha Cha ha a da Ca 120 G 1 JFlex input operators N return symbol HyPA_ASCII_sym CONCAT return symbol HyPA_ASCII_sym AND T BAX ZH return symbol HyPA ASCII sym 0R T wom return symbol HyPA_ASCII_sym SAT cjmp return symbol HyPA ASCII sym CJMP T gt gt return symbol HyPA_ASCII_sym REINITOP T wt return symbol HyPA ASCII sym ALTERNATIVEOP T Wen return symbol HyPA_ASCII_sym SEQUENTIALOP T gt return symbol HyPA_ASCII_sym DISRUPTOP L gt return symbol HyPA_ASCII_sym LDISRUPTOP MN return symbol HyPA ASCII sym PARALLELOP T DNE return symbol HyPA_ASCII_sym LPARALLELOP encap return symbol HyPA ASCII sym ENCAP T rename return symbol HyPA ASCII sym ACTIONRENAME T varrename return symbol HyPA_ASCII_sym VARRENAME T identifiers Identifier return symbol HyPA ASCII
151. zations during the simulation Status Deleted Updating the visualizations is much less time consuming than the simulation pro cess and it serves as a progress indication ID 29 Priority 18 Description The number of steps to undo can be indicated by the user in the message sequence charts Motivation Status Deleted Message Sequence Charts are no longer part of the requirements 28 3 2 Requirements 3 2 5 Modularity We anticipate several future extensions of the tool other input file formats additional types of visualizations other equation solvers and other clause formalisms ID 2 Priority 1 Description By adding a class and a reference other file formats can be read Motivation Amending the simulator such that it reads other file formats should not be difficult In order to make this requirement verifiable we specifically state that the addition of a class should be sufficient Status Partially fulfilled New parsers can be added easily but there is not yet a mechanism for choosing other file formats ID 4 Priority 5 Description Another differential equation solver can easily be used Motivation Supporting only one mathematical solver severely limits the usability of the simulator since not all users have access to the same solvers Status Not fulfilled The only clause formalisms currently implemented are the

Download Pdf Manuals

Related Search

Related Contents

manuel des pièces de rechange no. de modèle pr6n22cha  Manuel du propriétaire - Hobie 16  Livret d`accueil  Cellular Line HELLOKMP3SPK1 loudspeaker  GPS定位手表说明书 - Sunsky  NTP 20 Boxter.indd - Migros  Fiche produit  eUSB sofun 4 Manual_OL  Philips AE1500W  PDF 3.34MB  

Copyright © All rights reserved. Failed to retrieve file