11 lines
323 B
Promela
11 lines
323 B
Promela
; To "run" a milestone service,
|
|
; - assert that it is both started and ready
|
|
; - that's it!
|
|
;
|
|
? <run-service <milestone ?m>> [
|
|
<service-state <milestone $m> started>
|
|
<service-state <milestone $m> ready>
|
|
$log ! <log "-" { service: <milestone $m> state: up }>
|
|
?- <log "-" { service: <milestone $m> state: down }>
|
|
]
|