-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathreachability.golden
More file actions
64 lines (60 loc) · 2.86 KB
/
Copy pathreachability.golden
File metadata and controls
64 lines (60 loc) · 2.86 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
# Reachable state space of model.json under the canonical semantics in FORMS.md.
# Code generated by tools/codegen/reachability; DO NOT EDIT.
#
# Companion to parity/trace.golden, which pins one of the maximal firing
# sequences below. This file pins the machine that trace is a path through.
#
# marking {place,place,...}, places sorted; {} is the empty marking
# enabled one 'transition -> successor' per enabled transition, sorted by
# transition name. The first is the one the canonical scheduling
# policy fires; a marking with none is terminal.
places BoiledWater,CoffeeBeans,CoffeeInPot,Cup,Filter,GroundCoffee,Payment,Pending,Sent,Water
transitions BoilWater,BrewCoffee,Credit,GrindBeans,PourCoffee,Send
initial {CoffeeBeans,Cup,Filter,Pending,Water}
markings 16
edges 26
terminals 1
marking {BoiledWater,CoffeeBeans,Cup,Filter,Payment}
GrindBeans -> {BoiledWater,Cup,Filter,GroundCoffee,Payment}
marking {BoiledWater,CoffeeBeans,Cup,Filter,Pending}
GrindBeans -> {BoiledWater,Cup,Filter,GroundCoffee,Pending}
Send -> {BoiledWater,CoffeeBeans,Cup,Filter,Sent}
marking {BoiledWater,CoffeeBeans,Cup,Filter,Sent}
Credit -> {BoiledWater,CoffeeBeans,Cup,Filter,Payment}
GrindBeans -> {BoiledWater,Cup,Filter,GroundCoffee,Sent}
marking {BoiledWater,Cup,Filter,GroundCoffee,Payment}
BrewCoffee -> {CoffeeInPot,Cup,Payment}
marking {BoiledWater,Cup,Filter,GroundCoffee,Pending}
BrewCoffee -> {CoffeeInPot,Cup,Pending}
Send -> {BoiledWater,Cup,Filter,GroundCoffee,Sent}
marking {BoiledWater,Cup,Filter,GroundCoffee,Sent}
BrewCoffee -> {CoffeeInPot,Cup,Sent}
Credit -> {BoiledWater,Cup,Filter,GroundCoffee,Payment}
marking {CoffeeBeans,Cup,Filter,Payment,Water}
BoilWater -> {BoiledWater,CoffeeBeans,Cup,Filter,Payment}
GrindBeans -> {Cup,Filter,GroundCoffee,Payment,Water}
marking {CoffeeBeans,Cup,Filter,Pending,Water}
BoilWater -> {BoiledWater,CoffeeBeans,Cup,Filter,Pending}
GrindBeans -> {Cup,Filter,GroundCoffee,Pending,Water}
Send -> {CoffeeBeans,Cup,Filter,Sent,Water}
marking {CoffeeBeans,Cup,Filter,Sent,Water}
BoilWater -> {BoiledWater,CoffeeBeans,Cup,Filter,Sent}
Credit -> {CoffeeBeans,Cup,Filter,Payment,Water}
GrindBeans -> {Cup,Filter,GroundCoffee,Sent,Water}
marking {CoffeeInPot,Cup,Payment}
PourCoffee -> {Payment}
marking {CoffeeInPot,Cup,Pending}
Send -> {CoffeeInPot,Cup,Sent}
marking {CoffeeInPot,Cup,Sent}
Credit -> {CoffeeInPot,Cup,Payment}
marking {Cup,Filter,GroundCoffee,Payment,Water}
BoilWater -> {BoiledWater,Cup,Filter,GroundCoffee,Payment}
marking {Cup,Filter,GroundCoffee,Pending,Water}
BoilWater -> {BoiledWater,Cup,Filter,GroundCoffee,Pending}
Send -> {Cup,Filter,GroundCoffee,Sent,Water}
marking {Cup,Filter,GroundCoffee,Sent,Water}
BoilWater -> {BoiledWater,Cup,Filter,GroundCoffee,Sent}
Credit -> {Cup,Filter,GroundCoffee,Payment,Water}
marking {Payment}
terminal
terminal {Payment}