Altered_Pump_Spec_Concurrency.lts

//  Group 9
//  Authors: Zack Coker, Alex Duda, An Wu, Mauricio Soto, and Shurui Zhou
//
// 17-651: FSP model of a simple infusion pump
//
// ASSUMPTIONS
// - The user can choose, in the setup phase, which item of info to enter next.
// - The s1imple enter_value action is a simple number pad where the user enters
//   numeric values.
// - There exist 'set' and 'cancel' buttons, which are the targets of press_set
//   and press_cancel.
// - When the user turns the unit off, the unit will be in a state as if it was
//   just plugged in.
//
//
// Set of actions that the user of the LTSA tool can control in an
// animation of this model.
//
menu UserControlMenu = {
     //Pump interactions
     plug_in, unplug, attempt_turn_on, turn_off,  accept_self_test, decline_self_test, lock_unit, unlock_unit,

    //Line interactions
    l.[1..NumLines].set_rate, l.[1..NumLines].change_rate, l.[1..NumLines].enter_value, l.[1..NumLines].clear_rate, 
    l.[1..NumLines].confirm_settings, l.[1..NumLines].connect_set,
    l.[1..NumLines].erase_and_unlock_line,
    l.[1..NumLines].flow_unblocked, 
    l.[1..NumLines].press_cancel, 
    l.[1..NumLines].press_set_for_main, l.[1..NumLines].press_set_for_bolus,  l.[1..NumLines].silence_alarm,   
    l.[1..NumLines].flow_blocked, l.[1..NumLines].start_setup,
    l.[1..NumLines].replace_medicine,
    l.[1..NumLines].unlock_line_and_change_dispense_type
}

//======================
// Constants and Ranges
//======================


const NumLines = 2

//
// States of the pump alarm
//
const AlarmActivated = 0    // Alarm currently active
const AlarmSilenced  = 1    // Alarm currently inactive

range AlarmStateT = AlarmActivated .. AlarmSilenced

//
// States of the pump settings
//
const ParamsNotSet = 2    // pump parameters not set yet
const ParamsSet    = 3    // pump parameters already set

range ParamsStateT = ParamsNotSet .. ParamsSet

//
// Locked/unlocked states of a line with respect to a pump channel
//
const LineUnlocked = 4  // line not locked into a pump channel 
const LineLocked   = 5  // line locked into a pump channel

range LineLockStateT = LineUnlocked .. LineLocked

//
// Locked/unlocked states of the pump unit
//
const UnitUnlocked = 6  // the keypad of the pump is not locked
const UnitLocked   = 7  // the keypad of the pump is locked

range UnitLockStateT = UnitUnlocked .. UnitLocked

//The different dispensing states of the machine
//0 is not dispensing
//1 is dispensing a bolus
//2 is for dispensing the main meds
const NO_MEDICINE = 0
const BOLUS = 1
const MAIN_MEDS = 2
//for states that can be dispensing or not dispensing
range DispenseSettings = NO_MEDICINE..MAIN_MEDS
//for states that have to have a dispensing type
range DispenseType = BOLUS .. MAIN_MEDS

//=====================
// Process Definitions
//=====================

PUMP = (plug_in -> POWER_OFF),


POWER_OFF = 
(
    attempt_turn_on -> (successful_power_check -> UPDATE |
                unsuccessful_power_check -> POWER_OFF |
                system_powers_off_from_battery_failure -> PUMP) |
    system_powers_off_from_battery_failure -> PUMP |
    turn_off -> PUMP
    
),

//attempt to update the soft-check library and continue whether the update passes or fails
UPDATE = 
(
    attempt_library_update -> SELF_TEST_DECISION |
    system_powers_off_from_battery_failure -> PUMP |
    turn_off -> PUMP
),

//allows the user to select if the machine safety check occurs
SELF_TEST_DECISION =
(
  accept_self_test -> SELF_TEST |
  decline_self_test -> START_PUMP_DISPENSE |
  system_powers_off_from_battery_failure -> PUMP |
    turn_off -> PUMP
),

//returns the result of the machine safety check
SELF_TEST = 
(
   confirmed_self_test ->  START_PUMP_DISPENSE|
   failed_self_test -> display_error_pump -> sound_alarm_pump -> SELF_ERROR_STATE | 
   system_powers_off_from_battery_failure -> PUMP |
    turn_off -> PUMP
),

//the error state of the safety check - rings the alarm until the machine is turned off
SELF_ERROR_STATE =
(
    sound_alarm_pump -> SELF_ERROR_STATE |
    system_powers_off_from_battery_failure -> PUMP |
    turn_off -> PUMP 
    
),


START_PUMP_DISPENSE =
(
   start_lines -> (system_powers_off_from_battery_failure -> PUMP |
                    turn_off -> PUMP |
                   lock_unit -> LOCKED_PUMP) 
),

UNLOCKED_PUMP = 
(
                   system_powers_off_from_battery_failure -> PUMP |
                   turn_off -> PUMP |
                   lock_unit -> LOCKED_PUMP
),

LOCKED_PUMP = 
(
                    system_powers_off_from_battery_failure -> PUMP |
                    turn_off -> PUMP |
                    unlock_unit -> UNLOCKED_PUMP 
).

LINE = (start_lines -> UNLOCKED_INITIAL_LINE |
        system_powers_off_from_battery_failure -> LINE),

UNLOCKED_INITIAL_LINE = 
    (
    start_setup -> SETUP[ParamsNotSet][LineUnlocked][0] 
    |
    system_powers_off_from_battery_failure -> LINE
    |
    turn_off -> LINE
    |
    lock_unit -> LOCKED_INITIAL_LINE
    ),

LOCKED_INITIAL_LINE = 
(
    system_powers_off_from_battery_failure -> LINE
    |
    turn_off -> LINE
    |
    unlock_unit -> UNLOCKED_INITIAL_LINE
    ),

//
// Pump in setup mode:
// - Once required pump parameters (just rate in this case) are set,
//   physical connections can be made and line can be locked
//
SETUP[params:ParamsStateT][lineLock:LineLockStateT][dispenseType:DispenseSettings] = 
(
  //  unplug -> UNPLUGGED
  //  |
  //  turn_off -> POWER_OFF
  //  |
    when (params == ParamsNotSet && lineLock == LineUnlocked)
        set_rate -> enter_value ->
            (press_set_for_bolus -> SETUP[ParamsSet][lineLock][1]
             |
             press_set_for_main -> SETUP[ParamsSet][lineLock][2]
             |
             press_cancel -> SETUP[ParamsNotSet][lineLock][0])
    |
    when (params == ParamsSet && lineLock == LineUnlocked)
        clear_rate -> SETUP[ParamsNotSet][lineLock][0]
    |
    when (params == ParamsSet && lineLock == LineUnlocked)
        connect_set -> purge_air -> lock_line -> SETUP[params][LineLocked][dispenseType]
    |
    when (lineLock == LineLocked && dispenseType != 0)
        confirm_settings -> DANGEROUS_AMOUNT_CHECK_START[dispenseType]
    |
    when (lineLock == LineLocked)
        erase_and_unlock_line -> SETUP[params][LineUnlocked][dispenseType]
    |
    system_powers_off_from_battery_failure -> LINE
    |
    turn_off -> LINE
),

//checks if the amount entered is dangerous for bolus or main meds
DANGEROUS_AMOUNT_CHECK_START[dispenseType:DispenseType] = 
(
  check_dangerous_amount -> DANGEROUS_AMOUNT_CHECK_RESULT[dispenseType] 
  |
  system_powers_off_from_battery_failure -> LINE
  |
  turn_off -> LINE
),

//returns the result of the check for dangerous amounts (works for bolus or main meds)
DANGEROUS_AMOUNT_CHECK_RESULT[dispenseType:DispenseType] = 
(
  amount_is_dangerous -> DOUBLE_CHECK_AMOUNT[dispenseType]|
  amount_is_safe -> LINE_DISPENSE[UnitUnlocked][dispenseType] |
  system_powers_off_from_battery_failure -> LINE |
  turn_off -> LINE
),

//allows the user to confirm entering a dangerous amount (works for bolus or main meds)
DOUBLE_CHECK_AMOUNT[dispenseType:DispenseType] = 
(
   accept ->  LINE_DISPENSE[UnitUnlocked][dispenseType]|
   decline -> SETUP[ParamsNotSet][LineUnlocked][dispenseType] |
   system_powers_off_from_battery_failure -> LINE |
   turn_off -> LINE
),


//
// Line in infusion mode:
// - Line is dispensing.
// - Errors could occur with the pump (e.g., line became pinched or plugged)
//
LINE_DISPENSE[unitLock:UnitLockStateT][dispenseType:DispenseType] =
(
    system_powers_off_from_battery_failure -> LINE
    |
    turn_off -> LINE
    |
    when (unitLock == UnitUnlocked)
        change_rate -> SETUP[ParamsSet][LineLocked][dispenseType]
    |
    when (unitLock == UnitUnlocked)
        unlock_line_and_change_dispense_type -> SETUP[ParamsNotSet][LineUnlocked][0]
    |
    when (unitLock == UnitUnlocked)
        lock_unit -> LINE_DISPENSE[UnitLocked][dispenseType]
    |
    when (unitLock == UnitLocked)
        unlock_unit -> LINE_DISPENSE[UnitUnlocked][dispenseType]
    |
    when (dispenseType == 2)dispense_main_med -> LINE_DISPENSE[unitLock][dispenseType]
    |
    when (dispenseType == 1)dispense_bolus_med -> LINE_DISPENSE[unitLock][dispenseType]
    |
    flow_blocked -> display_error -> sound_alarm -> LINE_BLOCKED[unitLock][AlarmActivated][dispenseType]
    |
    medicine_is_empty -> display_error -> sound_alarm -> MEDICINE_EMPTY_ERROR_STATE[unitLock][AlarmActivated][dispenseType]
),

//
// medicine empty (medication flow suspended)
//
MEDICINE_EMPTY_ERROR_STATE[unitLock:UnitLockStateT][alarm:AlarmStateT][dispenseType:DispenseType] =
(
    
    turn_off -> LINE
    |
    system_powers_off_from_battery_failure -> LINE
    |
    when (alarm == AlarmActivated)
        sound_alarm -> MEDICINE_EMPTY_ERROR_STATE[unitLock][alarm][dispenseType]
    |
    when (alarm == AlarmActivated)
        silence_alarm -> MEDICINE_EMPTY_ERROR_STATE[unitLock][AlarmSilenced][dispenseType]
    |
    replace_medicine -> LINE_DISPENSE[unitLock][dispenseType]
),


//
// Pump stuck (medication flow suspended)
//
LINE_BLOCKED[unitLock:UnitLockStateT][alarm:AlarmStateT][dispenseType:DispenseType] =
(
    system_powers_off_from_battery_failure -> LINE 
    |   
    turn_off -> LINE
    |
    when (alarm == AlarmActivated)
        sound_alarm -> LINE_BLOCKED[unitLock][alarm][dispenseType]
    |
    when (alarm == AlarmActivated)
        silence_alarm -> LINE_BLOCKED[unitLock][AlarmSilenced][dispenseType]
    |
    flow_unblocked -> LINE_DISPENSE[unitLock][dispenseType]
).

property IT_WILL_DISPLAY_AN_ERROR_AFTER_LINE_FAILURE = (flow_blocked -> display_error->IT_WILL_DISPLAY_AN_ERROR_AFTER_LINE_FAILURE 
| medicine_is_empty -> display_error->IT_WILL_DISPLAY_AN_ERROR_AFTER_LINE_FAILURE).

progress EVENTUALLY_DISPENSE_MEDICINE = {l.[1..NumLines].dispense_main_med}

const PluggedIn = 0
const UnPlugged = 1
range PlugState = PluggedIn .. UnPlugged

const WallPowerWorking = 0
const WallPowerNotWorking = 1
range WallPowerState = WallPowerWorking ..WallPowerNotWorking

POWER_SYSTEM = (plug_in -> WALL_POWER |
                unsuccessful_power_check -> POWER_SYSTEM),


WALL_POWER = (
  unplug -> BATTERY_POWER[UnPlugged][WallPowerWorking]  |
  unplug ->  system_powers_off_from_battery_failure -> RESTORE_POWER[UnPlugged][WallPowerWorking] |
  wall_power_loss -> BATTERY_POWER[PluggedIn][WallPowerNotWorking] |
  wall_power_loss ->  system_powers_off_from_battery_failure -> RESTORE_POWER[PluggedIn][WallPowerNotWorking] |
  successful_power_check -> WALL_POWER
),

BATTERY_POWER[plugState:PlugState][currentWallPowerState:WallPowerState] = (
  when (plugState == UnPlugged && currentWallPowerState == WallPowerWorking) 
          plug_in -> WALL_POWER |
  when (plugState == UnPlugged && currentWallPowerState == WallPowerNotWorking) 
          plug_in -> BATTERY_POWER[PluggedIn][WallPowerNotWorking] |
  when (plugState == UnPlugged && currentWallPowerState == WallPowerNotWorking) 
          wall_power_restored -> BATTERY_POWER[UnPlugged][WallPowerWorking]|
  when (plugState == PluggedIn && currentWallPowerState == WallPowerNotWorking) 
          wall_power_restored -> WALL_POWER |
  when (plugState == PluggedIn) 
     unplug -> BATTERY_POWER[UnPlugged][currentWallPowerState] |
  system_powers_off_from_battery_failure -> RESTORE_POWER[plugState][currentWallPowerState] |
  successful_power_check -> BATTERY_POWER[plugState][currentWallPowerState]
  
),

RESTORE_POWER[plugState:PlugState][currentWallPowerState:WallPowerState] = (
    when(plugState == UnPlugged && currentWallPowerState == WallPowerNotWorking) 
        plug_in -> RESTORE_POWER[PluggedIn][currentWallPowerState] |
    when(plugState == UnPlugged && currentWallPowerState == WallPowerNotWorking) 
        wall_power_restored -> RESTORE_POWER[UnPlugged][WallPowerWorking] |
    when(plugState == UnPlugged && currentWallPowerState == WallPowerWorking) 
        plug_in -> WALL_POWER |
    when(plugState == PluggedIn && currentWallPowerState == WallPowerNotWorking)
        wall_power_restored -> WALL_POWER |
    when (plugState == PluggedIn) 
        unplug -> RESTORE_POWER[UnPlugged][currentWallPowerState] |
    unsuccessful_power_check -> RESTORE_POWER[plugState][currentWallPowerState]
  ).

const False = 0
const True = 1
fluent NoPower = <{plug_in,wall_power_restored},{system_powers_off_from_battery_failure}> initially False

assert NO_PUMP_AFTER_BATTERY_FAILURE = !<>(exists [i:1..NumLines](l.[i].dispense_main_med || l.[i].dispense_bolus_med) && !NoPower) 

fluent AFTER_FAILURE = <{flow_blocked, medicine_is_empty, system_powers_off_from_battery_failure}, {turn_off, dispense_main_med, dispense_bolus_med}>

assert RESUME_AFTER_FAILURE_POSSIBLE = [](AFTER_FAILURE -> <>(!turn_off && (dispense_main_med || dispense_bolus_med)))

property SOUND_ALARM_AFTER_FAILURE = (
	display_error -> sound_alarm -> SOUND_ALARM_AFTER_FAILURE
).

property CONFIRM_TO_DISPENSE = ( confirm_settings -> CONFIRMED |
                         system_powers_off_from_battery_failure -> CONFIRM_TO_DISPENSE |
                         turn_off -> CONFIRM_TO_DISPENSE),
CONFIRMED = (
  confirm_settings -> CONFIRMED |
  system_powers_off_from_battery_failure -> CONFIRM_TO_DISPENSE |
  dispense_main_med -> CONFIRMED |
  dispense_bolus_med -> CONFIRMED |
  turn_off -> CONFIRM_TO_DISPENSE).

//assert NO_PUMP_AFTER_BATTERY_FAILURE = []((!NoPower) -> 
//   !<>(exists [i:1..NumLines](l.[i].dispense_main_med || l.[i].dispense_bolus_med)))

//assert NO_PUMP_AFTER_BATTERY_FAILURE = [](system_powers_off_from_battery_failure -> !<>(exists [i:1..NumLines](l.[i].dispense_main_med || l.[i].dispense_bolus_med)))

|| INFUSION_PUMP = (PUMP || l[1..NumLines]:LINE || POWER_SYSTEM 
|| l[1..NumLines]:IT_WILL_DISPLAY_AN_ERROR_AFTER_LINE_FAILURE || l.[1]:CONFIRM_TO_DISPENSE ||
l.[2]:CONFIRM_TO_DISPENSE || l.[1]:SOUND_ALARM_AFTER_FAILURE || l.[2]:SOUND_ALARM_AFTER_FAILURE)/
{system_powers_off_from_battery_failure/l.[1..NumLines].system_powers_off_from_battery_failure,
turn_off/l.[1..NumLines].turn_off,
start_lines/l.[1..NumLines].start_lines,
lock_unit/l.[1..NumLines].lock_unit, 
unlock_unit/l.[1..NumLines].unlock_unit}.