New IOSA syntax for clock reset (non-Markovian)
Proposed new syntax:
module S1
on1: bool init true;
clkF1: clock~exponential(alpha1); // Clock for 'F'ailing
clkR1: clock~exponential(alpha0); // Clock for 'R'epairing
clkP1: clock~exponential(lambda); // Clock for 'P'roducing
// Breakdowns
[f1!] on1 @ clkF1 -> (on1'= false) & reset(clkR1);
[r1!] !on1 @ clkR1 -> (on1'= true) & reset(clkF1,clkP1);
// Production
[p1!] on1 @ clkP1 -> reset(clkP1);
endmodule
Equivalent to the old syntax (models/atm_queue.sa):
module S1
on1: bool init true;
clkF1: clock; // Clock for 'F'ailing ~ exponential(alpha1)
clkR1: clock; // Clock for 'R'epairing ~ exponential(alpha0)
clkP1: clock; // Clock for 'P'roducing ~ exponential(lambda)
// Breakdowns
[f1!] on1 @ clkF1 -> (on1'= false) &
(clkR1'= exponential(alpha0));
[r1!] !on1 @ clkR1 -> (on1'= true) &
(clkF1'= exponential(alpha1)) &
(clkP1'= exponential(lambda));
// Production
[p1!] on1 @ clkP1 -> (clkP1'= exponential(lambda));
endmodule