You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
12 lines
407 B
12 lines
407 B
domain FState = {NOMINAL, LOST, ERROR} ; |
|
domain FailureType = {Err, Loss, Ok} ; |
|
|
|
node Function |
|
flow I : FailureType : in ; O : FailureType : out ; |
|
state S : FState ; |
|
event fail_loss, fail_err ; |
|
init S := NOMINAL ; |
|
trans S != LOST |- fail_loss -> S := LOST ; |
|
S = NOMINAL |- fail_err -> S := ERROR ; |
|
assert O = case { S = NOMINAL : I, S = LOST : Loss, else Err } ; |
|
edon |