-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathpython.tmpl
More file actions
77 lines (65 loc) · 1.77 KB
/
Copy pathpython.tmpl
File metadata and controls
77 lines (65 loc) · 1.77 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
65
66
67
68
69
70
71
72
73
74
75
76
77
{{define "main" -}}
"""Code generated by tools/codegen from model.json; DO NOT EDIT.
Generated form: a scheduler loop over transitions whose arcs have been unrolled
into straight-line conditionals. Nothing walks an arrow list at runtime.
See FORMS.md.
"""
def initial_marking():
"""The marking is a set of marked place names. The net is 1-safe."""
return { {{- quoteAll .Initial -}} }
def render(marking):
"""Canonical trace rendering: marked places, sorted, comma-joined."""
return ",".join(sorted(marking))
{{range .Transitions}}
def fire_{{snake .Name}}(marking):
"""Check enablement, then apply.
Every check precedes every mutation, so a disabled transition leaves the
marking untouched.
"""
{{- range .Inputs}}
if "{{.}}" not in marking:
return False
{{- end}}
{{- range .Guards}}
if "{{.}}" not in marking: # guard
return False
{{- end}}
{{- range .Blockers}}
if "{{.}}" in marking: # inhibitor
return False
{{- end}}
{{- range .Outputs}}
if "{{.}}" in marking:
return False
{{- end}}
{{- range .Inputs}}
marking.discard("{{.}}")
{{- end}}
{{- range .Outputs}}
marking.add("{{.}}")
{{- end}}
return True
{{end}}
# Sorted transition order — deterministic, and not necessarily the order the
# interpreter form declares.
SCHEDULE = [
{{- range .Transitions}}
("{{.Name}}", fire_{{snake .Name}}),
{{- end}}
]
def main():
marking = initial_marking()
step = 0
while True:
fired = False
for name, fire in SCHEDULE:
if fire(marking):
step += 1
print(f"Step #{step}: {name} => {render(marking)}")
fired = True
break
if not fired:
return
if __name__ == "__main__":
main()
{{end}}