==================================
MODEL: tank.smv, sat_tank.xml
AUTHOR: Gabriele Zacco
==================================

A simple model of a tank.


MODEL
=====

The tank model is composed of:

- a tank
- a user request which can be either 0 (no request) or 1 (request to be served)
- an input flow
- an input valve, which can be either opened or closed
- an output valve, which can be either opened or closed
- a controller for the tank. The controller issues commands for the two valves
  (open or close) depending on the water level and the user request. The
  controller must ensure that the water level in the tank remains in a
  suitable range (not high, not low)

See further comments in the source file.

FAILURE MODES
=============

- flow failure
  type = "ramp_down_1_0"
  nusmv_node = flow_type.output
  description: the input flow fails and goes down to zero
    (amount = 1 at each step)

- valve stuck opened
  type = "stuck_at_opened"
  nusmv_node = valve_type.status
  description: a valve failing stuck opened

- valve stuck closed
  type = "stuck_at_closed"
  nusmv_node = valve_type.status
  description: a valve failing stuck closed

SAFETY REQUIREMENTS
===================

- PROP formula for FAULT TREE generation
  formula: "tank.water_level >= 100"
  description: tank overflow condition

- PROP formula for FAULT TREE generation
  formula: "tank.water_level = 0"
  description: tank underflow condition

- PROP formula for FAULT TREE generation
  formula: "tank.water_level >= 80"
  description: tank high level condition

- PROP formula for FAULT TREE generation
  formula: "tank.water_level <= 20"
  description: tank low level condition

- CTL property
  formula = "AG (flow_in.output_FailureMode = no_failure &
    valve_in.status_FailureMode != stuck_at_closed -> tank.water_level > 0)"
  description: tank never empties provided input flow does not fail and
    input valve does not fail stuck closed. This property holds

- CTL property
  formula = "flow_in.output_FailureMode != no_failure ->
    AF (tank.water_level <= 20)"
  description: if input flow fails, eventually tank level will be low.
    This property does not hold (consider the case in which there is no
    water request)