|
timeout 0.5 |
|
|
|
external 'door' |
|
|
|
function('min', [] => :integer) {1000} |
|
function('max', [] => :integer) {9999} |
|
|
|
process ('door'){ |
|
channel ('door') { |
|
stimuli 'open', 'close' |
|
responses 'opened', 'closed', 'locked', 'unlocked', 'invalid_command', 'invalid_passcode', 'incorrect_passcode', 'shut_off' |
|
|
|
stimulus 'lock', 'passcode' => :integer |
|
stimulus 'unlock', 'passcode' => :integer |
|
|
|
} |
|
|
|
var 'code', :integer |
|
var 'tries', :integer, 1 |
|
|
|
state 'closed' |
|
choice { |
|
o { receive 'open'; send 'opened'; goto 'opened' } |
|
o { receive 'close'; send 'invalid_command'; goto 'closed'} |
|
o { receive 'lock', constraint: 'passcode < min() || passcode > max()'; send 'invalid_passcode'; goto 'closed'} |
|
o { receive 'lock', constraint: 'passcode >= min() && passcode <= max()', update: 'code = passcode'; send 'locked'; goto 'locked'} |
|
o { receive 'unlock', constraint: 'passcode == passcode'; send 'invalid_command'; goto 'closed'} |
|
} |
|
|
|
state 'opened' |
|
choice { |
|
o { receive 'close'; send 'closed'; goto 'closed'} |
|
o { receive 'open'; send 'invalid_command'; goto 'opened' } |
|
o { receive 'lock', constraint: 'passcode == passcode'; send 'invalid_command'; goto 'opened' } |
|
o { receive 'unlock', constraint: 'passcode == passcode'; send 'invalid_command'; goto 'opened' } |
|
} |
|
|
|
state 'locked' |
|
choice { |
|
o { receive 'unlock', constraint: 'passcode < min() || passcode > max()'; send 'invalid_passcode'; goto 'locked'} |
|
o { receive 'unlock', update: 'tries = 1', constraint: 'passcode == code'; send 'unlocked'; goto 'closed'} |
|
o { receive 'unlock', constraint: 'tries < 3 && (passcode >= min() && passcode <= max()) && passcode != code ', update: 'tries = tries + 1'; send 'incorrect_passcode'; goto 'locked'} |
|
o { receive 'unlock', constraint: 'tries > 2 && (passcode >= min() && passcode <= max()) && passcode != code'; goto 'stop'} |
|
o { receive 'lock', constraint: 'passcode == passcode'; send 'invalid_command'; goto 'locked'} |
|
o { receive 'open' ; send 'invalid_command'; goto 'locked'} |
|
o { receive 'close'; send 'invalid_command'; goto 'locked'} |
|
} |
|
|
|
state 'stop' |
|
send 'incorrect_passcode' |
|
send 'shut_off' |
|
} |
