--------------------------------------

 Running NuSMV to verify the contract
            27/07/2007

--------------------------------------

--------------------------------------
- Running NuSMV in interactive mode:

nusmv -int

--------------------------------------
- Loading up the model in NuSMV:

reset
read_model -i C1.smv
flatten_hierarchy
encode_variables
build_model
print_reachable_states
check_fsm

--------------------------------------
- The contract semantic properties we want to check

  The translation process:

  O(a)  = <a> O_a
  F(a)  = [a] F_a
  <a> b = can_a & (a -> X b)
  [a] b = a -> X b
  <>  a = F a
  []  a = G a

  -- Property 1
  check_ltlspec -p "G((fi -> X F_fi) & (fi -> X (can_s & (s -> !F_s))))"
  -- Property 2
  check_ltlspec -p "G(h -> X (high -> ( (can_p & (p=1 -> X O_p)) & ((can_dn & ((d & n) -> X (O_d & O_n)))))))"
  -- Property 3
  check_ltlspec -p "G((d&n) -> X( (can_l & (l -> X O_l)) & (l -> X (F (can_pp & (p=2 -> X O_pp))))))"
  -- Property 4
  check_ltlspec -p "G((d&n) -> X(negl -> X(F(can_ppp & (p=3 -> X O_ppp)))))"
  -- Combining property 5
  check_ltlspec -p "G(o -> X(can_sfD & (sfD -> X O_sfD)))"

  Properties 1, 2 and 4 go through without any problem. Property 3 does not go through 
  because the property depends on property 2 (after the d&l which is mentioned in 
  property 2). The resulting property is:

  -- Combining properties 2 and 3:
  check_ltlspec -p "G(h -> X (high -> ( (can_p & (p=1 -> X O_p)) & ((can_dn & ((d & n) -> X (( (can_l & (l -> X O_l)) & (l -> X (F (can_pp & (p=2 -> X O_pp))))) & O_d & O_n)))))))"

  Property 4 is similar, but still goes through.

  Property 5 also does not go through due to a problem with the original contract. 
  Nothing in the contract specifies that the activation of the service (o) happens
  once, or that the user's obligation is only valid the first time the activation occurs.
  We restate the property as follows: 

  -- Fixing property 5:
  check_ltlspec -p "(!o) U (o -> X(can_sfD & (sfD -> X O_sfD)))"

--------------------------------------
- A properties we want to check

  check_ltlspec -p "G (!high | (p = 1 -> X (p = 1 -> X !O_p)))"

  This is not satified and we change our model to C2.smv to make it work 
  as expected.

  reset
  read_model -i C2.smv
  flatten_hierarchy
  encode_variables
  build_model
  print_reachable_states
  check_fsm

  We recheck the property which now holds:

  check_ltlspec -p "G (!high | (p = 1 -> X (p = 1 -> X !O_p)))" 

--------------------------------------
- A properties we want to check

  check_ltlspec -p "G(high -> ((d&n) -> X(l -> X( (h -> X F_h) U done_pp ))))"

  This fails leading us to modify the model to C2.smv

--------------------------------------