Skip to content

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