CIF simulator unsupported message for time-dependent state invariants is not specific enough
I have the following model
// Moving Arm // // Stopping arm is not instantaneous. // Stopping is initiated when // * position is beyond min or max position // * motor is stopped (c_stop) plant automaton Gear: controllable event c_up, c_down; disc real sgn = 1; location Up: initial; marked; edge c_down do sgn := -1 goto Down; location Down: edge c_up do sgn := 1 goto Up; end plant automaton Motor: controllable event c_start, c_stop; cont speed; const real MAX_VELOCITY = 10; invariant SpeedIdle: Idle => speed = 0; invariant SpeedRunning: Running => speed = MAX_VELOCITY; const real ACCELERATE = 1; const real DECELERATE = -2; location Idle: initial; marked; equation speed' = 0; edge c_start goto Accelerating; location Accelerating: equation speed' = ACCELERATE; edge when speed >= MAX_VELOCITY do speed := MAX_VELOCITY // Ensure invariant SpeedRunning despite numerical inaccuracies goto Running; edge c_stop goto Decelerating; location Running: equation speed' = 0; edge c_stop goto Decelerating; location Decelerating: equation speed' = DECELERATE; edge when speed <= 0 do speed := 0 // Ensure invariant SpeedIdle despite numerical inaccuracies goto Idle; edge c_start goto Accelerating; end const int MIN_POSITION = -1000; const int MAX_POSITION = 1000; group Arm: cont pos = 0 der Gear.sgn * Motor.speed; alg bool minSensor = pos <= MIN_POSITION; alg bool maxSensor = pos >= MAX_POSITION; end plant invariant shiftGearUp: Gear.c_up needs Motor.Idle; plant invariant shiftGearDown: Gear.c_down needs Motor.Idle; requirement invariant beyondMin: Arm.minSensor => not ((Motor.Accelerating or Motor.Running) and Gear.Down); requirement invariant beyondMax: Arm.maxSensor => not ((Motor.Accelerating or Motor.Running) and Gear.Up);
When I trigger
CIF simulation, validation and verification tools > Simulate CIF specifications..., click ok.
ERROR: Time dependent invariants are currently not supported by the CIF simulator: "Arm.minSensor => not((Motor.Accelerating or Motor.Running) and Gear.Down)".
This invariant is imho a timed state/event exclusion invariant, which is supported by the simulator. Do you agree? If so, please fix the bug. If not, please explain why it is indeed a time dependent invariant.