Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in
  • E escet
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Graph
    • Compare revisions
    • Locked files
  • Issues 94
    • Issues 94
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 9
    • Merge requests 9
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test cases
  • Deployments
    • Deployments
    • Releases
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Eclipse ProjectsEclipse Projects
  • Eclipse ESCET (Supervisory Control Engineering Toolkit)
  • escet
  • Issues
  • #513
Closed
Open
Issue created Jan 17, 2023 by Pierre van de Laar@pjljvandelaar

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

Assignee
Assign to
Time tracking

Copyright © Eclipse Foundation, Inc. All Rights Reserved.     Privacy Policy | Terms of Use | Copyright Agent