==================================
MODEL: adder.smv, sat_adder.xml
AUTHOR: Marco Bozzano
==================================

A very simple model of a six-bit adder.


MODEL
=====

The "bit" module models a component which takes an input variable
representing the value of a bit, and simply copies it to an output
variable.  The "adder" module takes in input the outputs of six bit
module instances, and computes their sum (modulo two).  Finally, the
"main" module defines the overall system, by instantiating an adder
and six different bit components, whose inputs are random Boolean
variables.

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

- corrupted_bit
  type = "inverted"
  nusmv_node = bit.output
  description: a corrupted input bit

- power failure
  type = "stuck_at_0"
  nusmv_node = adder.output
  description: power failure stucks the output of the adder to zero

- short circuit
  type = "stuck_at_1"
  nusmv_node = adder.output
  description: short circuit stucks the output of the adder to one

FAILURE SETS
============

- fs-bit1-bit2
  type = simultaneous
  components = bit1.output_FailureMode = inverted,
               bit2.output_FailureMode = inverted
  description = this FS models a simultaneous failure of bit1 and bit2

- fs-bit2-bit3
  type = simultaneous
  components = bit2.output_FailureMode = inverted,
               bit3.output_FailureMode = inverted
  description = this FS models a simultaneous failure of bit2 and bit3

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

- CTL property
  formula = "AG ((random1 = 0 & random2 = 0 & random3 = 0 & random4 = 0 &
    random5 = 0 & random6 = 0 & adder.output != 0) ->
    (bit1.output_FailureMode = inverted | bit2.output_FailureMode = inverted |
     bit3.output_FailureMode = inverted | bit4.output_FailureMode = inverted |
     bit5.output_FailureMode = inverted | bit6.output_FailureMode = inverted))"
  description: If "0+0+0+0+0+0 is not equal to 0", then one of the inputs is
    corrupted. This property may be false (e.g., in case of a short circuit)

- CTL property
  formula = "AG ((random1 = 0 & random2 = 0 & random3 = 0 & random4 = 0 &
    random5 = 0 & random6 = 0 & adder.output != 0) ->
    (adder.output_FailureMode != stuck_at_0))"
  description: If "0+0+0+0+0+0 is not equal to 0", then power has not failed.
    This property holds

- PROP formula for FAULT TREE generation
  formula: "random1 = 0 & random2 = 0 & random3 = 0 & random4 = 0 &
    random5 = 0 & random6 = 0 & adder.output != 0"
  description: We want to instigate events causing the sum 0+0+0+0+0+0 to be
    different from 0