I need to model that an event means something different if it happens twice in quick succession than if it happens widely separated in time. My first thought was to have a seq of functions to say wha to do next, and cycle through it, but I found seq too difficult to work with. So, I’ve tried to brute force a countdown on transitions. This works:
sig StateHolder{
,var countdown: Int
}
fact trace{
all s: StateHolder | s.countdown = 3
always one s: StateHolder | {
s.countdown' = larger[0, minus[s.countdown,1]]
all x : StateHolder - s | x.countdown' = x.countdown
}
}
run {
eventually
all s: StateHolder | zero[s.countdown]
} for exactly 1 StateHolder, 6 Time
but, I need more than one StateHolder, and this doesn’t have any instances:
sig StateHolder{
,var countdown: disj Int
}
fact trace{
all s: StateHolder | s.countdown = 3
always one s: StateHolder | {
s.countdown' = larger[0, minus[s.countdown,1]]
all x : StateHolder - s | x.countdown' = x.countdown
}
}
run {
eventually
all s: StateHolder | zero[s.countdown]
} for exactly 2 StateHolder, 12 Time
There are two issues that prevent Electrum from building an infinite trace:
The disj in the declaration of field countdown prevents the same integer to be in the countdown of two different state holders. However, both counters must go to 0 before looping forever. Just remove disj.
The one in the fact trace also prevents the looping behaviour when both counters reach 0, because at that point both state holders must satisfy the constraint s.countdown' = larger[0, minus[s.countdown,1]] and you are requiring that only one will do so. Just replace one by some.
It could be that this timing issue should be below the level of abstraction of the model. In a user interface model, for example, you wouldn’t model selection with one click and open with double click as the same event, but would just treat them as two distinct event types. The question I would ask is this: what do you gain by explicitly modeling the timing here? And if it is a real issue, can it be separated out into a model that you use to analyze an interpretation layer?
That’s the spec. It says: when the vehicle operator presses the “unlock cargo” button on the remote control the rear cargo door opens, and if they press it again within two seconds, the side cargo door also opens.
An interesting question is: what happens if they press the “unlock [people]” button in between ? The users’ manual is silent on this, I need to get at a real vehicle. If I model press and double-press as different kinds of instantaneous events I can’t talk about that gap.
can it be separated out into a model that you use to analyze an interpretation layer
I strongly suspect that there is a module on the CAN bus which does exactly that, interpreting wireless signals from the remote and sending unlock messages to the door controllers. Why/how would I model that separately?
