Formulaquotient generates an "Error in parity_game_generator" when generating and writing intermediate results, on the experiment in Variant 3:
This seems to work fine:
mcrl22network.py ../exampleXY.mcrl2
formulaquotient -v -IPS -nexampleXY.net ../reach.mcf example.reachY.pbes
But this results in an error:
mcrl22network.py ../exampleXY.mcrl2
formulaquotient -v -IPSFN -nexampleXY.net ../reach.mcf example.reachY.pbes
yields the following error message:
[11:24:51 verbose] writing modal equation system to file 'reach_1.mes'...
[11:24:51 verbose] Saving result in pbes format...
[11:24:51 verbose] Generating parity game...
[11:24:51 verbose] Error in parity_game_generator: unexpected expression 3 == 0
[11:24:51 error] DataAppl(OpId(==,SortArrow([SortId(Nat),SortId(Nat)],SortId(Bool)),96),DataAppl(OpId(@cnat,SortArrow([SortId(Pos)],SortId(Nat)),6),DataAppl(OpId(@cdub,SortArrow([SortId(Bool),SortId(Pos)],SortId(Pos)),1),OpId(true,SortId(Bool),7),OpId(@c1,SortId(Pos),3))),OpId(@c0,SortId(Nat),19))
Formulaquotient generates an "Error in parity_game_generator" when generating and writing intermediate results, on the experiment in Variant 3:
This seems to work fine:
mcrl22network.py ../exampleXY.mcrl2
formulaquotient -v -IPS -nexampleXY.net ../reach.mcf example.reachY.pbes
But this results in an error:
mcrl22network.py ../exampleXY.mcrl2
formulaquotient -v -IPSFN -nexampleXY.net ../reach.mcf example.reachY.pbes
yields the following error message:
[11:24:51 verbose] writing modal equation system to file 'reach_1.mes'...
[11:24:51 verbose] Saving result in pbes format...
[11:24:51 verbose] Generating parity game...
[11:24:51 verbose] Error in parity_game_generator: unexpected expression 3 == 0
[11:24:51 error] DataAppl(OpId(==,SortArrow([SortId(Nat),SortId(Nat)],SortId(Bool)),96),DataAppl(OpId(@cnat,SortArrow([SortId(Pos)],SortId(Nat)),6),DataAppl(OpId(@cdub,SortArrow([SortId(Bool),SortId(Pos)],SortId(Pos)),1),OpId(true,SortId(Bool),7),OpId(@c1,SortId(Pos),3))),OpId(@c0,SortId(Nat),19))