MACHINE T_m1_prob_real
CONCRETE_CONSTANTS
  A /*@desc constant positive acceleration */,
  b /*@desc constant negative acceleration */,
  e /*@desc "cycle time of controller" */,
  sl
ABSTRACT_VARIABLES
  phase2,
  a2,
  v2,
  z2,
  a,
  m,
  v,
  z,
  phase
/* PROMOTED OPERATIONS
  get_limit,
  decide_1,
  decide_2,
  decide_3,
  drive_1,
  drive_2,
  decide_1_2,
  decide_2_2,
  decide_3_2,
  drive_1_2,
  drive_2_2 */
PROPERTIES
    /* @T_c0:axm1 */ 0.0 < e /*@desc every e seconds the controller acts */
  & /* @T_c0:axm2 */ 0.0 < A /*@desc constant positive acceleration */
  & /* @T_c0:axm3 */ 0.0 < b /*@desc constant negative acceleration */
  & /* @T_c0:prob-ignore-axm5 */ !(x,y).(
     not(y = 0.0)
     =>
     y * (x / y) = x
    ) /*@desc prob-ignore */
  & /* @T_c0:axm6 */ b = 1.0
  & /* @T_c0:axm7 */ A = 2.0
  & /* @T_c0:axm9 */ e = 2.0
  & /* @T_c0:axm10 */ 0.0 < sl /*@desc should be at least 4 to avoid DLK!! */
  & /* @T_c0:axm11 */ !x.(
     0.0 <= x
     =>
     0.0 <= 2.0 * ((x * x) / 2.0)
    ) /*@desc prob-ignore */
  & /* @T_c0_prob:prob-sl */ sl = 5.0
INVARIANT
    /* @T_m1:inv1 */ phase2 : {0,1,2}
  & /* @T_m1:inv2 */ 0.0 <= z2
  & /* @T_m1:inv3 */ a2 : {0.0,A,- b}
  & /* @T_m1:inv4 */ 0.0 <= v2
  & /* @T_m1:inv5 */ v2 * v2 <= 2.0 * z - 2.0 * z2
  & /* @T_m1:inv7 */ (
     (
      phase2 = 2
      &
      v2 + 2.0 * a2 <= 0.0
     )
     =>
     a2 = - b
    )
  & /* @T_m1:inv8 */ (
     (
      phase2 = 2
      &
      a2 = A
     )
     =>
     v2 * v2 + (24.0 + 12.0 * v2) <= 2.0 * z - 2.0 * z2
    )
  & /* @T_m1:inv9 */ (
     (
      phase2 = 2
      &
      a2 = 0.0
     )
     =>
     v2 * v2 + (24.0 + 12.0 * v2) <= 2.0 * z - 2.0 * z2
    )
  & /* @T_m0:inv1 */ phase : {0,1,2}
  & /* @T_m0:inv3 */ 0.0 <= z
  & /* @T_m0:inv4 */ a : {0.0,A,- b} /*@desc acceleration of train */
  & /* @T_m0:inv5 */ 0.0 <= v
  & /* @T_m0:inv10 */ 0.0 <= m
  & /* @T_m0:inv7 */ v * v <= 2.0 * m - 2.0 * z /*@desc 2∗b∗m−2∗b∗z≥v∗v */
  & /* @T_m0:inv8 */ (
     (
      phase = 2
      &
      v + 2.0 * a <= 0.0
     )
     =>
     a = - b
    ) /*@desc phase=2 ∧ v+e∗a≤0 ⇒ a=−b   (e=2) */
  & /* @T_m0:inv9 */ (
     (
      phase = 2
      &
      a = A
     )
     =>
     v * v + (24.0 + 12.0 * v) <= 2.0 * m - 2.0 * z
    ) /*@desc phase=2 ∧ a=A ⇒ m−z ≥ v∗v + 5∗e∗e + 5∗e∗v
     (e=2) */
  & /* @T_m0:inv11 */ (
     (
      phase = 2
      &
      a = 0.0
     )
     =>
     v * v + (24.0 + 12.0 * v) <= 2.0 * m - 2.0 * z
    )
ASSERTIONS
     /* @T_c0:axm8 */ A * b = 2.0
   ; /* @T_m1:inv6 */ 0.0 <= z - z2
   ; /* @T_m0:inv6 */ 0.0 <= m - z /*@desc SAFETY CONDITION: the train position z is
     always situated BEFORE the limit position m */
INITIALISATION
    BEGIN
         phase := 1
      ||
         z := 0.0
      ||
         v := 0.0
      ||
         a := 2.0
      ||
         m := 0.0
      ||
         phase2 := 1
      ||
         z2 := 0.0
      ||
         a2 := 0.0
      ||
         v2 := 0.0
    END
OPERATIONS
  get_limit = 
    ANY x
    WHERE 
        /* @T_m1_prob:grd1 */ x : 1 .. 300
      & /* @T_m1_prob:grd3 */ v = 0.0
      & m - z < 12.0 /*@desc 2∗b∗m−2∗b∗z < v∗v + A∗e∗e∗b + A∗e∗e∗A + 2∗e∗v∗b + 2∗e∗v∗A

v = 0
A = 2
e = 2
b = 1

2*b*m-2*b*z < A∗e∗e∗b + A∗e∗e∗A = 24 */
      & /* @T_m1_prob:grd5 */ m = 0.0
    THEN
      m := m + real(x)
    END;
  
  decide_1 = 
    SELECT 
        /* @T_m1_prob:grd1 */ phase = 1
      & 2.0 * m - 2.0 * z < v * v + (24.0 + 12.0 * v) /*@desc 2∗b∗m−2∗b∗z < v∗v + A∗e∗e∗b+ A∗e∗e∗A + 2∗e∗v∗b + 2∗e∗v∗A
         b = 1
         A = 2
         e = 2 */
      & /* @T_m1_prob:grd4 */ 0.0 < v
    THEN 
         a := - b
      ||
         phase := 2
    END;
  
  decide_2 = 
    SELECT 
        /* @T_m1_prob:grd1 */ phase = 1
      & v * v + (24.0 + 12.0 * v) <= 2.0 * m - 2.0 * z /*@desc 2∗b∗m−2∗b∗z ≥ v∗v + A∗e∗e∗b+ A∗e∗e∗A + 2∗e∗v∗b + 2∗e∗v∗A
         v∗v + 24 + 12∗v */
      & v + 4.0 <= sl /*@desc v+e∗A (e=2, A=2) */
    THEN 
         a := 2.0
      ||
         phase := 2
    END;
  
  decide_3 = 
    SELECT 
        /* @T_m1_prob:grd1 */ phase = 1
      & v * v + (24.0 + 12.0 * v) <= 2.0 * m - 2.0 * z /*@desc 2∗b∗m−2∗b∗z ≥ v∗v + A∗e∗e∗b+ A∗e∗e∗A + 2∗e∗v∗b + 2∗e∗v∗A
         v∗v + 24 + 12∗v */
      & sl < v + 4.0 /*@desc v+e∗A (e=2, A=2) */
      & /* @T_m1_prob:grd7 */ 0.0 < v
    THEN 
         a := 0.0
      ||
         phase := 2
    END;
  
  drive_1 = 
    SELECT 
        /* @T_m1_prob:grd1 */ phase = 2
      & v + 2.0 * a <= 0.0 /*@desc v+e∗a≤0  (e=2) */
    THEN 
         v := 0.0
      ||
         z := z + (v * v) / 2.0
      ||
         phase := 1
    END;
  
  drive_2 = 
    SELECT 
        /* @T_m1_prob:grd2 */ phase = 2
      & 0.0 < v + 2.0 * a /*@desc v+e∗a>0 (e=2) */
    THEN 
      v,z,phase := v + 2.0 * a,z + (2.0 * v + 2.0 * a),1
    END;
  
  decide_1_2 = 
    SELECT 
        /* @T_m1_prob:grd1 */ phase2 = 1
      & /* @T_m1_prob:grd2 */ 2.0 * z - 2.0 * z2 < v2 * v2 + (24.0 + 12.0 * v2)
      & /* @T_m1_prob:grd3 */ 0.0 < v2
    THEN 
         a2 := - b
      ||
         phase2 := 2
    END;
  
  decide_2_2 = 
    SELECT 
        /* @T_m1_prob:grd1 */ phase2 = 1
      & /* @T_m1_prob:grd2 */ v2 * v2 + (24.0 + 12.0 * v2) <= 2.0 * z - 2.0 * z2
      & /* @T_m1_prob:grd3 */ v2 + 4.0 <= sl
    THEN 
         phase2 := 2
      ||
         a2 := 2.0
    END;
  
  decide_3_2 = 
    SELECT 
        /* @T_m1_prob:grd1 */ phase2 = 1
      & /* @T_m1_prob:grd2 */ v2 * v2 + (24.0 + 12.0 * v2) <= 2.0 * z - 2.0 * z2
      & /* @T_m1_prob:grd3 */ sl < v2 + 4.0
      & /* @T_m1_prob:grd4 */ 0.0 < v2
    THEN 
         a2 := 0.0
      ||
         phase2 := 2
    END;
  
  drive_1_2 = 
    SELECT 
        /* @T_m1_prob:grd1 */ phase2 = 2
      & /* @T_m1_prob:grd2 */ v2 + 2.0 * a2 <= 0.0
    THEN 
         v2 := 0.0
      ||
         z2 := z2 + (v2 * v2) / 2.0
      ||
         phase2 := 1
    END;
  
  drive_2_2 = 
    SELECT 
        /* @T_m1_prob:grd1 */ phase2 = 2
      & /* @T_m1_prob:grd2 */ 0.0 < v2 + 2.0 * a2
    THEN 
      v2,z2,phase2 := v2 + 2.0 * a2,z2 + (2.0 * v2 + 2.0 * a2),1
    END
DEFINITIONS
 "LibrarySVG.def";
 SET_PREF_USE_IGNORE_PRAGMAS == TRUE;

/* DEFINITIONS
  EXPRESSION MAX == 
  30;
  EXPRESSION VISB_SVG_OBJECTS3a;
  EXPRESSION VISB_SVG_OBJECTS3b;
  EXPRESSION WIDTH;
  EXPRESSION XOffset == 
  10;
  EXPRESSION VISB_SVG_CONTENTS;
  EXPRESSION VISB_JSON_FILE;
  EXPRESSION VISB_SVG_BOX;
  EXPRESSION xcoord(x);
  EXPRESSION DOMPOS;
  EXPRESSION NEXTTRAIN(Nr,zpos,vpos,Col);
  EXPRESSION SET_PREF_USE_IGNORE_PRAGMAS == 
  TRUE;
  EXPRESSION TEXT_FIELD(MYID,X,Y,Width,Height,Fontsize);
  EXPRESSION VISB_SVG_OBJECTS1;
  EXPRESSION VISB_SVG_OBJECTS2;
  EXPRESSION DOM;
  EXPRESSION vehLen;
  EXPRESSION Scale;
  EXPRESSION HEIGHT;
  EXPRESSION VISB_SVG_OBJECTS4;
  EXPRESSION TRAIN(Nr,zpos,vpos,apos,Col);
  EXPRESSION VISB_SVG_OBJECTS5;
  EXPRESSION VISB_SVG_OBJECTS6;
  EXPRESSION VISB_SVG_OBJECTS7; */
END