import os

os.system('mcrl22lps -nv leader.mcrl2 leader.lps')

os.system('lps2pbes -v -f nodeadlock.mcf leader.lps leader.nodeadlock.pbes')
os.system('pbes2bool -v leader.nodeadlock.pbes')

# This indicates the size of the non-reduces state space
os.system('lps2lts -v leader.lps')

# Find and eliminate the constants representing process id's
os.system('lpsconstelm -v leader.lps temp.lps')

# Find confluent taus and rename these to ctau. The flag -o enables induction on
# lists, which is necessary to prove confluence
os.system('lpsconfcheck -o temp.lps temp1.lps')

# This shows the dramatically reduced statespace, generated by giving priority
# to ctaus.
os.system('lps2lts -vcctau temp1.lps temp1.svc')



