# /* BRP - iz magisterija */
# /* Robert Meolic, 5. 9. 2003 */

pa_read_process "brp.dat"
pa_encode_process "SENDER RECEIVER CHANNELK CHANNELL TIMERS"
pa_encode_process "BRP_weak BRP_test BRP_trace"

versis_compose 1 BRP \
  "SENDER RECEIVER CHANNELK CHANNELL TIMERS" \
  "REQ SOK SNOK SDK RFST RINC ROK RNOK"

versis_strong_minimization 1 BRP
versis_weak_minimization 1 BRP
versis_trace_minimization 1 BRP

outline ""

out "COMPOSITION BRP: "
out [pa_comp_state_number BRP]
out " st, "
out [pa_comp_transition_number BRP]
out " tr, "
out [pa_comp_transition_visible BRP]
outline " vis"

out "STRONG_BRP: "
out [pa_state_number STRONG_BRP]
out " st, "
out [pa_transition_number STRONG_BRP]
out " tr, "
out [pa_transition_visible STRONG_BRP]
outline " vis"

out "WEAK_BRP: "
out [pa_state_number WEAK_BRP]
out " st, "
out [pa_transition_number WEAK_BRP]
out " tr, "
out [pa_transition_visible WEAK_BRP]
outline " vis"

out "TRACE_BRP: "
out [pa_state_number TRACE_BRP]
out " st, "
out [pa_transition_number TRACE_BRP]
out " tr, "
out [pa_transition_visible TRACE_BRP]
outline " vis"

out "BRP_weak: "
out [pa_state_number BRP_weak]
out " st, "
out [pa_transition_number BRP_weak]
out " tr, "
out [pa_transition_visible BRP_weak]
outline " vis"

out "BRP_test: "
out [pa_state_number BRP_test]
out " st, "
out [pa_transition_number BRP_test]
out " tr, "
out [pa_transition_visible BRP_test]
outline " vis"

out "BRP_trace: "
out [pa_state_number BRP_trace]
out " st, "
out [pa_transition_number BRP_trace]
out " tr, "
out [pa_transition_visible BRP_trace]
outline " vis"

outline ""

versis_strong_equivalence 0 STRONG_BRP 1 BRP
versis_weak_equivalence 0 WEAK_BRP 1 BRP
versis_trace_equivalence 0 TRACE_BRP 1 BRP

versis_strong_equivalence 0 BRP_weak 1 BRP
versis_strong_equivalence 0 BRP_test 1 BRP
versis_strong_equivalence 0 BRP_trace 1 BRP

versis_weak_equivalence 0 BRP_weak 1 BRP
versis_weak_equivalence 0 BRP_test 1 BRP
versis_weak_equivalence 0 BRP_trace 1 BRP

versis_testing_equivalence 0 BRP_weak 1 BRP
versis_testing_equivalence 0 BRP_test 1 BRP
versis_testing_equivalence 0 BRP_trace 1 BRP

versis_trace_equivalence 0 BRP_weak 1 BRP
versis_trace_equivalence 0 BRP_test 1 BRP
versis_trace_equivalence 0 BRP_trace 1 BRP

versis_weak_equivalence 0 WEAK_BRP 0 BRP_weak
versis_trace_equivalence 0 TRACE_BRP 0 BRP_trace

versis_testing_equivalence 0 STRONG_BRP 0 BRP_test
versis_testing_equivalence 0 WEAK_BRP 0 BRP_test
versis_testing_equivalence 0 TRACE_BRP 0 BRP_test
