selfcheck : CONTEXT =
BEGIN
 
sensor_data: TYPE;

actuator_data: TYPE;
init: actuator_data;

laws(x: sensor_data): actuator_data;

ideal: MODULE =
BEGIN
INPUT
  data_in: sensor_data
OUTPUT
  ideal_out: actuator_data
INITIALIZATION
  ideal_out = init;
TRANSITION
  ideal_out' = laws(data_in)
END;
 
 
metasignal: TYPE = {up, down};

controller: MODULE =
BEGIN
INPUT
  data_in: sensor_data
OUTPUT
  control_out: actuator_data,
  errorflag: metasignal
INITIALIZATION
  control_out = init;
  errorflag = down;
TRANSITION
[
normal:
  TRUE --> control_out' = laws(data_in); errorflag' = down;
[]
hardware_fault:
  TRUE --> control_out' IN {x: actuator_data | x /= laws(data_in)}; errorflag' = up;
]
END;
 
 
monitor: MODULE = ideal || controller;

check_nonfaulty: LEMMA monitor |- G(errorflag = down => control_out = ideal_out);
 
 
% sal-inf-bmc selfcheck.sal check_nonfaulty -d 10
 
 
% true by 1-induction
% sal-inf-bmc selfcheck.sal check_nonfaulty -i -d 1 -v 1
 
 
check_faulty: LEMMA monitor |- G(errorflag = up => control_out /= ideal_out);
 
 
check_controller: LEMMA monitor |- G(errorflag = up <=> control_out /= ideal_out);
 
 
% true by 1-induction
% sal-inf-bmc selfcheck.sal check_faulty -i -d 1 -v 1

% true by 1-induction
% sal-inf-bmc selfcheck.sal check_controller -i -d 1 -v 1
 
 
checker: MODULE = 
BEGIN
INPUT
  con_out: actuator_data,
  mon_out: actuator_data
OUTPUT
  safe_out: actuator_data,
  fault: boolean
INITIALIZATION
 safe_out = init;
 fault = FALSE;
TRANSITION
safe_out' = con_out';
[
disagree:
  con_out' /= mon_out' --> fault' = TRUE
[]
ELSE --> 
]
END;
 
 
cpair: MODULE = checker
 || (RENAME control_out TO con_out, errorflag TO cerror IN controller)
 || (RENAME control_out TO mon_out, errorflag TO merror IN controller);
 
 
test_cpair1: LEMMA cpair |- G((cerror = up OR merror = up) => fault);
 
 
test_cpair2: LEMMA cpair |- G((cerror = up XOR merror = up) => fault);
 
 
test_cpair3: LEMMA cpair |- G(fault => (cerror = up OR merror = up));
 
 
test_cpair4: LEMMA cpair |- G((NOT fault AND X(fault)) => X(cerror = up OR merror = up));
 
 
% sal-inf-bmc selfcheck.sal test_cpair1 -v 1
% sal-inf-bmc selfcheck.sal test_cpair1 -it -v 1
% sal-inf-bmc selfcheck.sal test_cpair2 -i -d 1 -v 1
% sal-inf-bmc selfcheck.sal test_cpair3 -v 1
% sal-inf-bmc selfcheck.sal test_cpair3 -it -v 1
% sal-inf-bmc selfcheck.sal test_cpair4 -i -d 2 -v 1
 
 
pair_assumptions: MODULE = 
BEGIN
OUTPUT
  commonflag: metasignal
INPUT
  data_in, c_data, m_data: sensor_data,
  cerror, merror: metasignal,
  con_out, mon_out: actuator_data
INITIALIZATION
 commonflag = down
TRANSITION
[
assumption_violation:
  (cerror' = up AND merror' = up AND con_out' = mon_out') --> commonflag' = up;
[]
usual:
  ELSE --> 
]
END;

test_cpair1_a: LEMMA cpair || pair_assumptions |- 
   G(commonflag = down => ((cerror = up OR merror = up) => fault));

test_cpair4_a: LEMMA cpair || pair_assumptions |- 
   G(commonflag = down => (NOT fault AND X(fault)) => X(cerror = up OR merror = up));
 
 
% sal-inf-bmc selfcheck.sal test_cpair1_a -i -d 1 -v 1
% sal-inf-bmc selfcheck.sal test_cpair4_a -i -d 2 -v 1
 
 
distributor: MODULE = 
BEGIN
INPUT
  data_in: sensor_data
OUTPUT
  c_data, m_data: sensor_data
INITIALIZATION
  c_data = data_in; m_data = data_in;
TRANSITION
[
distributor_ok:
  TRUE --> c_data' = data_in'; m_data' = data_in';
[]
distributor_bad:
  TRUE --> c_data' IN {x: sensor_data | TRUE};  m_data' IN {y: sensor_data | TRUE};
]
END;
 
 
full_cpair: MODULE = distributor || checker
 || (RENAME control_out TO con_out, data_in TO c_data, errorflag TO cerror IN controller)
 || (RENAME control_out TO mon_out, data_in to m_data, errorflag TO merror IN controller);

test_cpair1_x: LEMMA full_cpair || pair_assumptions |- 
   G(commonflag = down => ((cerror = up OR merror = up) => fault));
 
 
% sal-inf-bmc selfcheck.sal test_cpair1_x -it
 
 
mod_assumptions: MODULE = 
BEGIN
OUTPUT
  commonflag: metasignal
INPUT
  data_in, c_data, m_data: sensor_data,
  cerror, merror: metasignal,
  con_out, mon_out: actuator_data
INITIALIZATION
 commonflag = down
TRANSITION
[
assumption_violation:
  (m_data' /= c_data' and mon_out' = con_out') OR
    (cerror' = up AND merror' = up AND con_out' = mon_out') --> commonflag' = up;
[]
usual:
  ELSE -->
]
END;
 
 
test_cpair1_b: LEMMA full_cpair || mod_assumptions |- 
   G(commonflag = down => ((cerror = up OR merror = up) => fault));

test_cpair4_b: LEMMA full_cpair || mod_assumptions |- 
   G(commonflag = down => (NOT fault AND X(fault)) => X(cerror = up OR merror = up));
 
 
mod2_assumptions: MODULE = 
BEGIN
OUTPUT
  commonflag: metasignal
INPUT
  data_in, c_data, m_data: sensor_data,
  cerror, merror: metasignal,
  con_out, mon_out: actuator_data
INITIALIZATION
 commonflag = down
TRANSITION
[
assumption_violation:
  (m_data' = c_data' AND m_data' /= data_in') OR
    (m_data' /= c_data' and mon_out' = con_out') OR
      (cerror' = up AND merror' = up AND con_out' = mon_out') --> commonflag' = up;
[]
usual:
  ELSE -->
]
END;

cpair_ok: LEMMA full_cpair || mod2_assumptions || ideal |- 
   G(commonflag = down => (NOT fault => safe_out = ideal_out));
 
 
% sal-inf-bmc selfcheck.sal test_cpair1_b -i -d 2 -v 1
% sal-inf-bmc selfcheck.sal test_cpair4_b -i -d 3 -v 1
% sal-inf-bmc selfcheck.sal cpair_ok -i -d 2 -v 1
 
END