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

A very simple model of a two-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 two bit
module instances, and computes their sum (modulo two).  Finally, the
"main" module defines the overall system, by instantiating an adder
and two 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


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

- CTL property
  formula = "AG ((random1 = 0 & random2 = 0 & adder.output != 0) ->
    (bit1.output_FailureMode = inverted | bit2.output_FailureMode = inverted))"
  description: If "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 & adder.output != 0) ->
    (bit1.output_FailureMode = inverted | bit2.output_FailureMode = inverted))"
  description: If "0+0 is not equal to 0", then then power has not failed.
    This property holds

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