MACHINE pillbox_final
SETS /* deferred */
  Drawer;
  Timer
 ; /* enumerated */
  LedLights={OFF,ON};
  Drugs={TYLENOL,ASPIRINE,MOMENT}
CONCRETE_CONSTANTS
  drawer1,
  drawer2,
  drawer3,
  tenMinutes
ABSTRACT_VARIABLES
  isPillTaken,
  drawerLed,
  time_consumption,
  drug,
  drugIndex,
  isPillTobeTaken,
  mCurrTimeSecs,
  start
/* PROMOTED OPERATIONS
  ENV_toggle_isPillTaken,
  r_Main,
  IncTimeByMinutes */
/* NOT PROMOTED OPERATIONS
  r_choosePillToTake,
  r_reset_timer,
  r_pillToBeTaken,
  r_setOtherDrawers,
  r_reset,
  r_take */
PROPERTIES
    Drawer = {drawer1,drawer2,drawer3}
  & card({drawer1,drawer2,drawer3}) = 3
INVARIANT
    isPillTaken : Drawer --> BOOL
  & drawerLed : Drawer --> LedLights
  & time_consumption : Drawer --> seq(INTEGER)
  & drug : Drawer --> Drugs
  & drugIndex : Drawer --> NATURAL
  & isPillTobeTaken : Drawer --> BOOL
  & mCurrTimeSecs : NATURAL
  & start : Timer --> NATURAL
  & !d.(
     drawerLed(d) = ON
     =>
     not(#d2.(d2 /= d & drawerLed(d2) = ON))
    )
INITIALISATION
    BEGIN
         drawerLed := Drawer * {OFF}
      ||
         time_consumption := {drawer1 |-> [60,1200,1800],drawer2 |-> [2400,3000,3600],drawer3 |-> [180,1200,1800]}
      ||
         drug := {drawer1 |-> TYLENOL,drawer2 |-> ASPIRINE,drawer3 |-> MOMENT}
      ||
         isPillTobeTaken := Drawer * {FALSE}
      ||
         drugIndex := Drawer * {1}
      ||
         isPillTaken := Drawer * {FALSE}
      ||
         mCurrTimeSecs := 0
      ||
         start := Timer * {0}
    END
OPERATIONS
  ENV_toggle_isPillTaken(d,newval) = 
    SELECT 
        newval = 
        bool(
            isPillTaken(d) = FALSE
        )
    THEN 
      isPillTaken(d) := newval
    END;
  
  IncTimeByMinutes(mins) = 
    SELECT 
        mins : {1,10,60}
    THEN 
      mCurrTimeSecs := mCurrTimeSecs + mins * 60
    END;
  
  ΔdrawerLed,ΔisPillTobeTaken <-- r_reset(drawers) = 
    BEGIN
      ΔdrawerLed,drugIndex,ΔisPillTobeTaken := drawers * {OFF},drugIndex <+ %drawer.(drawer : drawers|drugIndex(drawer) + 1),drawers * {FALSE}
    END;
  
  ΔdrawerLed,ΔisPillTobeTaken <-- r_take(drawers) = 
    LET iftrue BE iftrue = {drawer|drawer : drawers & drawerLed(drawer) = ON & (mCurrTimeSecs >= start(tenMinutes) + 600 or isPillTaken(drawer) = TRUE)}
    IN
      ΔdrawerLed,ΔisPillTobeTaken <-- r_reset(iftrue)
    END;
  
  ΔdrawerLed,ΔisPillTobeTaken1,ΔisPillTobeTaken2 <-- r_setOtherDrawers = 
    BEGIN
         ΔisPillTobeTaken1 := %(drawer) . (
             drugIndex(drawer) : dom(time_consumption(drawer))
           & time_consumption(drawer)(drugIndex(drawer)) <= mCurrTimeSecs
           & drawerLed(drawer) = OFF
          | 
           TRUE
         )
      ||
         LET other BE other = {drawer|drugIndex(drawer) <= size(time_consumption(drawer))}
         IN
           ΔdrawerLed,ΔisPillTobeTaken2 <-- r_take(other)
         END
    END;
  
  r_reset_timer(t) = 
    BEGIN
      start(t) := mCurrTimeSecs
    END;
  
  ΔdrawerLed <-- r_pillToBeTaken(drawer) = 
    BEGIN
         IF drawerLed(drawer) = OFF THEN
           r_reset_timer(tenMinutes)
         END
      ||
         ΔdrawerLed := {drawer |-> ON}
    END;
  
  ΔdrawerLed <-- r_choosePillToTake = 
    LET cands BE cands = {drawer|isPillTobeTaken(drawer) = TRUE & drawerLed(drawer) = OFF & not(#d2.(d2 /= drawer & drawerLed(d2) = ON))}
    IN
      IF cands /= {} THEN
        ANY drawer
        WHERE 
            drawer : cands
        THEN
          ΔdrawerLed <-- r_pillToBeTaken(drawer)
        END
      ELSE
        ΔdrawerLed := {}
      END
    END;
  
  concurrent_updates <-- r_Main = 
    VAR ΔdrawerLed1,ΔdrawerLed2,ΔisPillTobeTaken1,ΔisPillTobeTaken2
    IN
           ΔdrawerLed1 <-- r_choosePillToTake
        ||
           ΔdrawerLed2,ΔisPillTobeTaken1,ΔisPillTobeTaken2 <-- r_setOtherDrawers
      ;
        drawerLed,isPillTobeTaken,concurrent_updates := drawerLed <+ (ΔdrawerLed1 \/ ΔdrawerLed2),isPillTobeTaken <+ (ΔisPillTobeTaken1 \/ ΔisPillTobeTaken2),(ΔdrawerLed1 \/ ΔdrawerLed2) |-> (ΔisPillTobeTaken1 \/ ΔisPillTobeTaken2)
    END
DEFINITIONS
 SET_PREF_STORE_DETAILED_TRANSITION_INFOS == TRUE;

/* DEFINITIONS
  EXPRESSION VISB_SVG_UPDATES3;
  EXPRESSION VISB_SVG_UPDATES2;
  EXPRESSION VISB_SVG_UPDATES5;
  EXPRESSION VISB_SVG_UPDATES4;
  EXPRESSION VISB_SVG_EVENTS3;
  EXPRESSION VISB_SVG_EVENTS1;
  EXPRESSION VISB_SVG_EVENTS2;
  EXPRESSION duration(t);
  EXPRESSION VISB_SVG_HOVERS3;
  PREDICATE expired(t);
  EXPRESSION VISB_SVG_HOVERS1;
  EXPRESSION VISB_SVG_HOVERS2;
  PREDICATE isOn(d);
  PREDICATE isOff(d);
  EXPRESSION ASSERT_CTL1;
  EXPRESSION isPillTaken_updates(d);
  EXPRESSION drawer_updates(d,col);
  EXPRESSION SET_PREF_STORE_DETAILED_TRANSITION_INFOS == 
  TRUE;
  PREDICATE drugIndexWD(d);
  PREDICATE isThereAnyOtherDeadline(d);
  EXPRESSION currentTime(t);
  EXPRESSION ASSERT_LTL1;
  EXPRESSION ASSERT_LTL2;
  PREDICATE pillDeadlineHit(d);
  EXPRESSION defaults;
  EXPRESSION VISB_SVG_FILE;
  EXPRESSION VISB_SVG_UPDATES1;
  PREDICATE areOthersOn(d);
  EXPRESSION ASSERT_LTL3; */
END