CIF simulator unsupported message for time-dependent state invariants is not specific enough
Dear Developers,
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.
I get
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.
Greetings, Pierre