# Train example verbose := 0; Automata : train1 [ Clocks : x1 Nodes : Far, Before, On Transitions : Far -App!, {x1} -> Before, Before -a, x1>20^x1<30, {x1} -> On, On -Exit!,x1>10^x1<20 -> Far Invariants : Before |= x1 < 30, On |= x1 < 20 Atomic Propositions : On |= ON ]; Automata : train2 [ Clocks : x2 Nodes : Far, Before, On Transitions : Far -App!, {x2} -> Before, Before -a, x2>20^x2<30, {x2} -> On, On -Exit!,x2>10^x2<20 -> Far Invariants : Before |= x2 < 30; On |= x2 < 20 Atomic Propositions : On |= ON ]; Automata : gate [ Clocks : Hg Nodes : Open, Close, Raising, Lowering Transitions : Open -GoDown?, {Hg} -> Lowering, Open -GoUp? -> Open, Lowering -GoDown? -> Lowering, Lowering -GoUp?, {Hg} -> Raising, Lowering -a, Hg<10 -> Close, Close -GoUp?, {Hg} -> Raising, Close -GoDown? -> Close, Raising -GoUp? -> Raising, Raising -GoDown?, {Hg} -> Lowering, Raising -a, Hg<10 -> Open Invariants : Lowering |= Hg<10; Raising |= Hg<10 Atomic Propositions : Open |= OPEN, Close |= CLOSE ]; Automata : controller [ Clocks : Hc Nodes : c0, c1, c2 Transitions : c0 - App?, {Hc} -> c2, c0 - Exit?, {Hc} -> c1, c2 - Exit? -> c2, c2 - App? -> c2, c2 - GoDown!, Hc<=10 -> c0, c1 - Exit? -> c1, c1 - App? -> c2, c1 - GoUp!, Hc=50 -> c0 Invariants : c1 |= Hc <= 50 , c2 |= Hc <= 10 ]; Table : T { (train1, train2 , controller, gate) ; (App!, ., App?, .) -> App ; (., App!, App?, .) -> App ; (Exit!, ., Exit?, .) -> Exit ; (., Exit!, Exit?, .) -> Exit ; (., ., GoUp!, GoUp?) -> GoUp; (., ., GoDown!, GoDown?) -> GoDown; (a, ., ., .) -> a; (., a, ., .) -> a; (., ., ., a) -> a; # the following rules are used for P3: (., ., Exit?, .) -> Exit? ; (Exit!, ., ., .) -> Exit! ; (., Exit!, ., .) -> Exit! }; System : S (train1 [1 1 0 1 0], train2, controller, gate[1 1 1 1 0]); # The numbers between [ ] defines which simplification rules are # applied after the quotienting. # The order of the processes gives also the order of the quotienting.