One shot perturbations ignore requested time

[hmedina]

When the user explicitly requests a one-shot perturbation, the float parameter specified for the alarm is discarded and the perturbation fires the first time it can. This is not what a "one shot perturbation with alarm" means.

Take the following example model:

%agent: deadlock(site{a,b})     %init: 2 deadlock()
deadlock(site{a}) <-> deadlock(site{b}) @ 1, 1

%agent: A()
%agent: B()

%mod: alarm 1 do $ADD 1 A() ;
%mod: alarm 2 do $ADD 1 B() ; repeat [false]

%obs: 'A' |A()|
%obs: 'B' |B()|

%mod: alarm 5 do $STOP ;

The time traces for the observables look like:

Note that agent B was added from the get-go, at what seems to be T=0, rather than at T=2, which is what the model specifies.

The run produces a witness file like:

%def: "seed" "490408346"
%def: "dumpIfDeadlocked" "true"
%def: "maxConsecutiveClash" "3"
%def: "progressBarSize" "70"
%def: "progressBarSymbol" "#"

%agent: deadlock(site{a b})
%agent: A()
%agent: B()

%var:/*0*/ 'A' |A()|
%var:/*1*/ 'B' |B()|
%plot: [T]
%plot: A
%plot: B

deadlock(site{a/b}[#]) @ 1
deadlock(site{b/a}[#]) @ 1

/*0*/%mod: alarm 1 ([T] > 0) do $APPLY 1 A()+; repeat [false]
/*1*/%mod: alarm 2 [true] do $APPLY 1 B()+; repeat [false]
/*2*/%mod: alarm 5 ([T] > 0) do $STOP ; repeat [false]

%init: 2 deadlock(site{a}[.])

When explicitly requesting to not repeat the perturbation, the internal translation does not edit the statement by adding the boolean component ([T]>0), instead just having a [true] token, as is seen above in the witness file; compare mod 0 and mod 1. Not repeating perturbation is the default; this leads to a situation where a user that explicitly requests a behavior that is default, does not get default behavior.

Moreover, the "guard" that is the boolean condition added ([T] > 0) does not get added if the statement already contained a boolean condition. Swapping:

%mod: alarm 1 do $ADD 1 A() ;

for

%mod: alarm 1 (|deadlock()| > 0) do $ADD 1 A() ;

Produces time traces where both A and B got added from the get-go; both perturbations now ignore the user-specified float parameter. The witness file will list the line as:

/*0*/%mod: alarm 1 (|deadlock()| > 0) do $APPLY 1 A()+; repeat [false]

Relying on this "guard" is both opaque, and error prone; we should not rely on re-interpreting the user's input. I suggest we either have some syntax for a true one-shot perturbation, or remove this guard and habituate users to add the [T]>0 component throughout our models.