plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/examples/tfpg/forgerobot/forgerobot.smv

--#define HMON(h_mon, var) VAR h_mon : boolean; INIT h_mon <-> var; TRANS next(h_mon) <-> (h_mon | next(var));

--------------------------------------------------------------------------------

MODULE forge_environment

  VAR workload : {low, mid, high};
  VAR heat : {low, high};

--------------------------------------------------------------------------------

MODULE forge_robot (env_workload, env_heat, time_delta, do_timed, done_timed)

  -- hack!
  TRANS non_crit_overheating != next(non_crit_overheating) -> position = next(position);
  TRANS crit_overheating != next(crit_overheating) -> position = next(position);

  -- discretization constraints
  TRANS heat_level < 10 -> !next(heat_level > 10);
  TRANS heat_level < 13 -> !next(heat_level > 13);
  TRANS heat_level < 15 -> !next(heat_level > 15);
  TRANS work_done < 6 -> !next(work_done > 6);

  VAR non_crit_overheating : boolean;
  ASSIGN init(non_crit_overheating) := FALSE;
  ASSIGN next(non_crit_overheating) := case
    heat_level >= 10 : TRUE;
    TRUE : FALSE;
    esac;

  --INVARSPEC (non_crit_overheating != next(non_crit_overheating)) -> !do_timed;

  VAR crit_overheating : boolean;
  ASSIGN init(crit_overheating) := FALSE;
  ASSIGN next(crit_overheating) := case
    heat_level >= 15 : TRUE;
    TRUE : FALSE;
    esac;

  --INVARSPEC (crit_overheating != next(crit_overheating)) -> !do_timed;

  -- robot position

  DEFINE can_move := !f_locomotion & heat_level < 13;

  VAR position : {critical_zone, safe_zone};
  ASSIGN init(position) := safe_zone;
  ASSIGN next(position) := case
    do_timed : position;
    !can_move : position;
    -- stay in critical zone until work is done
    position=critical_zone & work_done < 6 : critical_zone;
    -- leave critical zone once work is done
    position=critical_zone & work_done = 6 : safe_zone;
    -- do not enter critical zone with positive heat level
    position=safe_zone & heat_level > 0 : safe_zone;
    -- random choice
    TRUE : {critical_zone, safe_zone};
    esac;

  -- robot heat level

  VAR heat_level : real;
  ASSIGN init(heat_level) := 0;
  ASSIGN next(heat_level) := case
    !do_timed : heat_level;
    -- heat development in safe zone
    position=safe_zone : max(0, heat_level - time_delta);
    -- heat development leaving critical zone
    position=critical_zone & next(position=safe_zone) : heat_level;
    -- heat development in critical zone
    f_cooling & env_heat = high : heat_level + time_delta * 2;
    TRUE : heat_level + time_delta;
    esac;

  --LTLSPEC G ((position=safe_zone & X (position=critical_zone)) -> heat_level=0);

  -- status of work in critical zone

  VAR work_done : real;
  ASSIGN init(work_done) := 6;
  ASSIGN next(work_done) := case
    -- no work
    next(position=safe_zone) : 6;
    -- start work
    position=safe_zone & next(position=critical_zone) : 0;
    -- doing work
    env_workload=low : work_done + time_delta * 3;
    env_workload=mid : work_done + time_delta * 2;
    TRUE : work_done + time_delta;
    esac;

  -- failure of robot cooling system (permanent)

  VAR f_cooling : boolean;
  TRANS f_cooling -> next(f_cooling);
  TRANS do_timed -> f_cooling=next(f_cooling);

  -- failure of robot locomotion (permanent)

  VAR f_locomotion : boolean;
  TRANS f_locomotion -> next(f_locomotion);
  TRANS do_timed -> f_locomotion=next(f_locomotion);

  --LTLSPEC G (f_cooling -> G f_cooling);
  --LTLSPEC G (f_locomotion -> G f_locomotion);

--------------------------------------------------------------------------------

MODULE main

  -- environment modeling amount of heat and workload in critical zone
  VAR environment : forge_environment;

  -- assume environment is stable when robot enters critical zone,
  -- but can be different each time the robot enters the zone.
  TRANS robot.position=critical_zone -> environment.workload = next(environment.workload);
  TRANS robot.position=critical_zone -> environment.heat = next(environment.heat);

  VAR robot : forge_robot(environment.workload, environment.heat, time_delta,
                          do_timed, done_timed);

  IVAR time_delta : real;
  FAIRNESS time_delta > 0;
  TRANS time_delta >= 0;

  -- guard to prevent discrete updates during timed transitions
  VAR do_timed : boolean;
  TRANS do_timed <-> time_delta > 0;
  TRANS do_timed -> !next(do_timed);

  -- guard to enable discrete updates after each timed transition
  VAR done_timed : boolean;
  INIT !done_timed;
  TRANS do_timed <-> next(done_timed);

  --INVARSPEC do_timed -> !done_timed;
  --INVARSPEC done_timed -> !do_timed;
  --LTLSPEC G F do_timed;


--  HMON(h_F_LOCOMOTION, robot.f_locomotion)
--  INVARSPEC time_delta=1 -> (h_F_LOCOMOTION = next(h_F_LOCOMOTION));
--
--  HMON(h_F_COOLING, robot.f_cooling)
--  INVARSPEC time_delta=1 -> (h_F_COOLING = next(h_F_COOLING));
--
--  DEFINE def_NON_CRITICAL_OVERHEATING:= robot.heat_level >= 10;
--  HMON(h_NON_CRITICAL_OVERHEATING, def_NON_CRITICAL_OVERHEATING)
--  INVARSPEC time_delta=1 -> (h_NON_CRITICAL_OVERHEATING = next(h_NON_CRITICAL_OVERHEATING));
--
--  DEFINE def_CRITICAL_OVERHEATING:= robot.heat_level = 15;
--  HMON(h_CRITICAL_OVERHEATING, def_CRITICAL_OVERHEATING)
--  INVARSPEC time_delta=1 -> (h_CRITICAL_OVERHEATING = next(h_CRITICAL_OVERHEATING));
--
--  DEFINE def_UNIT_STUCK:= !robot.can_move;
--  HMON(h_UNIT_STUCK, def_UNIT_STUCK)
--  INVARSPEC time_delta=1 -> (h_UNIT_STUCK = next(h_UNIT_STUCK));