pa_read_process "dme-martin.dat"
pa_read_process "dme-smv.dat"
pa_encode_process "dme-martin-dat-false-phd dme-martin-dat-false"
pa_encode_process "dme-martin-dat-true-phd dme-martin-dat-true"
pa_encode_process "dme-smv-dat-false-phd dme-smv-dat-false"
pa_encode_process "dme-smv-dat-true-phd dme-smv-dat-true"

set dir [pwd]; cd ../circuits; source init.tcl; cd $dir
ccs_read ../circuits-dme/dme-martin.ccs
ccs_read ../circuits-dme/dme-smv.ccs

outline "dme-martin-dat-false-phd has [pa_state_number dme-martin-dat-false-phd] states / [pa_transition_number dme-martin-dat-false-phd] transitions / [bdd_node_number D_dme-martin-dat-false-phd] BDD nodes."
outline "dme-martin-dat-false has [pa_state_number dme-martin-dat-false] states / [pa_transition_number dme-martin-dat-false] transitions / [bdd_node_number D_dme-martin-dat-false] BDD nodes."
outline "DME-MARTIN-FALSE has [pa_state_number DME-MARTIN-FALSE] states / [pa_transition_number DME-MARTIN-FALSE] transitions / [bdd_node_number D_DME-MARTIN-FALSE] BDD nodes."
outline ""
outline "dme-martin-dat-true-phd has [pa_state_number dme-martin-dat-true-phd] states / [pa_transition_number dme-martin-dat-true-phd] transitions / [bdd_node_number D_dme-martin-dat-true-phd] BDD nodes."
outline "dme-martin-dat-true has [pa_state_number dme-martin-dat-true] states / [pa_transition_number dme-martin-dat-true] transitions / [bdd_node_number D_dme-martin-dat-true] BDD nodes."
outline "DME-MARTIN-TRUE has [pa_state_number DME-MARTIN-TRUE] states / [pa_transition_number DME-MARTIN-TRUE] transitions / [bdd_node_number D_DME-MARTIN-TRUE] BDD nodes."

outline ""

outline "dme-smv-dat-false-phd has [pa_state_number dme-smv-dat-false-phd] states / [pa_transition_number dme-smv-dat-false-phd] transitions / [bdd_node_number D_dme-smv-dat-false-phd] BDD nodes."
outline "dme-smv-dat-false has [pa_state_number dme-smv-dat-false] states / [pa_transition_number dme-smv-dat-false] transitions / [bdd_node_number D_dme-smv-dat-false] BDD nodes."
outline "DME-SMV-FALSE has [pa_state_number DME-SMV-FALSE] states / [pa_transition_number DME-SMV-FALSE] transitions / [bdd_node_number D_DME-SMV-FALSE] BDD nodes."
outline ""
outline "dme-smv-dat-true-phd has [pa_state_number dme-smv-dat-true-phd] states / [pa_transition_number dme-smv-dat-true-phd] transitions / [bdd_node_number D_dme-smv-dat-true-phd] BDD nodes."
outline "dme-smv-dat-true has [pa_state_number dme-smv-dat-true] states / [pa_transition_number dme-smv-dat-true] transitions / [bdd_node_number D_dme-smv-dat-true] BDD nodes."
outline "DME-SMV-TRUE has [pa_state_number DME-SMV-TRUE] states / [pa_transition_number DME-SMV-TRUE] transitions / [bdd_node_number D_DME-SMV-TRUE] BDD nodes."

outline ""

versis_trace_equivalence 0 dme-martin-dat-false 0 dme-martin-dat-false-phd
versis_trace_equivalence 0 dme-martin-dat-true 0 dme-martin-dat-true-phd
versis_trace_equivalence 0 dme-smv-dat-false 0 dme-smv-dat-false-phd
versis_trace_equivalence 0 dme-smv-dat-true 0 dme-smv-dat-true-phd

outline ""

versis_trace_equivalence 0 dme-martin-dat-false 0 DME-MARTIN-FALSE
versis_trace_equivalence 0 dme-martin-dat-true 0 DME-MARTIN-TRUE
versis_trace_equivalence 0 dme-smv-dat-false 0 DME-SMV-FALSE
versis_trace_equivalence 0 dme-smv-dat-true 0 DME-SMV-TRUE

outline ""

versis_testing_equivalence 0 dme-martin-dat-false 0 DME-MARTIN-FALSE
versis_testing_equivalence 0 dme-martin-dat-true 0 DME-MARTIN-TRUE
versis_testing_equivalence 0 dme-smv-dat-false 0 DME-SMV-FALSE
versis_testing_equivalence 0 dme-smv-dat-true 0 DME-SMV-TRUE

outline ""

versis_strong_equivalence 0 dme-martin-dat-false 0 DME-MARTIN-FALSE
versis_strong_equivalence 0 dme-martin-dat-true 0 DME-MARTIN-TRUE
versis_strong_equivalence 0 dme-smv-dat-false 0 DME-SMV-FALSE
versis_strong_equivalence 0 dme-smv-dat-true 0 DME-SMV-TRUE
