-- the level of the tank ranges from 0 to 100
-- a level > 80 is high
-- a level < 20 is low

#define LEVEL_HI  (water_level > 80)
#define LEVEL_LOW (water_level < 20)

-- the default flow out of the tank

#define TANK_FLOW_OUT 5

-- auxiliary definitions

#define min(a,b) case a < b: a; a >= b: b; esac
#define max(a,b) case a > b: a; a <= b: b; esac

-------------------------------------------------------------------------------
MODULE flow_type(input)

-- models system input flow

VAR
  output : 0..10;

ASSIGN
  output := input;


-------------------------------------------------------------------------------
MODULE valve_type(flow_in,command)

-- models input and output valves of the tank
-- a valve can be closed or opened

VAR
  flow_out : 0..10;
  status   : {opened,closed};

-- the status of the valve changes depending on the command issued by
-- the controller (open or close)

ASSIGN
  init(status) := closed;
  next(status) := case
                    command = open  : opened;
                    command = close : closed;
                  esac;

-- is the valve is opened, it outputs the flow it receives as input
-- if the valve is closed, there is no output flow

ASSIGN
  flow_out := case
                status = opened : flow_in;
                status = closed : 0;
              esac;

-------------------------------------------------------------------------------
MODULE tank_type(flow_in,valve_out_status)

-- models the tank
-- the water level is always between 0 and 100
-- the input flow is given as input
-- the output flow is between 0 and 5

VAR
  water_level : 0..100;
  flow_out    : 0..5;  

-- initially the output flow is 0
-- at each step, the output flow is the minimum between the water level
-- and TANK_FLOW_OUT

ASSIGN
  init(flow_out) := 0;
  next(flow_out) := min(water_level,TANK_FLOW_OUT);

-- initially, the water level is 50
-- at each step:
-- if the output valve is opened,
-- the water level is increased by the input flow (coming from the input
-- valve) and descreased by TANK_FLOW_OUT
-- if the output valve is closed,
-- the water level is increased by the input flow (coming from the input
-- valve)
-- the water level is forced to be always between 0 and 100

ASSIGN
  init(water_level) := 50;
  next(water_level) := case
    valve_out_status = opened : min(100,max(0,water_level + flow_in - TANK_FLOW_OUT));
    valve_out_status = closed : min(100,water_level + flow_in);
  esac;


-------------------------------------------------------------------------------
MODULE user_type

-- models a non-deterministic user request
-- "0" means no request, "1" means a request to be served

VAR
  get_water : {0,1};

ASSIGN
  init(get_water) := 0;
  next(get_water) := {0,1};


-------------------------------------------------------------------------------
MODULE controller_type(water_level,user_request)

-- models the controller
-- the controller issues commands (either open or close) for
-- the input and output valve

VAR
  command_in  : {open,close};
  command_out : {open,close};

-- the controller closes the input valve if the water level in the tank is
-- high, or the level is normal and there is no user request
-- the controller opens the input valve if the water level in the tank is
-- low, or the level is normal and there is a user request

ASSIGN
  init(command_in) := close;
  next(command_in) := case
                        LEVEL_HI     : close;
                        LEVEL_LOW    : open;
                        user_request : open;
                        1            : close;
                      esac;

-- the controller opens the output valve if the water level in the tank is
-- high, or the level is nornal and there is a user request
-- the controller closes the output valve if water level in the tank is
-- low, or the level is normal and there is no user request

  init(command_out) := close;
  next(command_out) := case
                         LEVEL_HI     : open;
                         LEVEL_LOW    : close;
                         user_request : open;
                         1            : close;
                       esac;

-------------------------------------------------------------------------------
MODULE main

-- the overall system is composed of:
--   a user request module
--   input flow (with flow equal to 5)
--   an input valve
--   the tank
--   an output valve
--   the controller

VAR
  user        : user_type;
  flow_in     : flow_type(5);
  valve_in    : valve_type(flow_in.output,controller.command_in);
  tank        : tank_type(valve_in.flow_out,valve_out.status);
  valve_out   : valve_type(tank.flow_out,controller.command_out);
  controller  : controller_type(tank.water_level,user.get_water);