# /* Robert Meolic, 14. 10. 1999 */
# /* Robert Meolic, last modified Jul 10, 2008 */
# /* Primer iz magisterija - simbolicno preverjanje z ACTL-jem. */

# known model checker's settings
global mc_diagnostic
global mc_automaton
global mc_explain
global mc_minimize
global mc_tracepath
global mc_progress

pa_read_process "crossing.dat"
pa_encode_process "cross train car"

versis_compose 0 crossing \
  "cross train car" \
  "isClose isOpen isRed isGreen lower raise"

outline ""

ccs_read crossing.ccs

pa_encode_process "CROSS TRAIN CAR"
versis_strong_equivalence 0 cross 0 CROSS
versis_strong_equivalence 0 train 0 TRAIN
versis_strong_equivalence 0 car 0 CAR

outline ""

versis_trace_equivalence 1 crossing 0 S
versis_testing_equivalence 1 crossing 0 S
versis_weak_equivalence 1 crossing 0 S
versis_strong_equivalence 1 crossing 0 S

outline ""

# MODEL CHECKING
mc_check_actl_file 0 S "crossing.actl" [expr $mc_diagnostic]
mc_check_actl 1 crossing crossing_F6 [expr $mc_diagnostic + $mc_explain + $mc_tracepath]

# WCA
#mc_check_actl 1 S crossing_F5 [expr $mc_automaton | $mc_minimize]
#mc_check_actl 1 S crossing_F6 [expr $mc_automaton | $mc_minimize]
