pbesiteration tool

[jacenre]

The tool performs fixpoint iteration on the PBES equations from bottom to top to reach a solution.
Current implementation uses EQBDDs to check if a fixpoint has been reached. In the future, we want to try using SAT solvers as well.
Also, with the -g flag (WIP), it will check if the main condition (core constraint) is a global invariant.

(See Property 29 and Proposition 38 of Orzan, Simona, and Tim A. C. Willemse. “Invariants for Parameterised Boolean Equation Systems.” Theoretical Computer Science 411, no. 11 (March 6, 2010): 1338–71. https://doi.org/10.1016/j.tcs.2009.11.001.)

---

TODO:

• If I load the marijkesluizen PBES specification of "no_deadlock", I get different results based on if I import it as a TXT formatted file or a regular binary file. In a binary file, it stalls (caused by memory issues?). In a TXT file, it runs fine.
  For instance, pbesiteration marijkesluizen.pbes versus pbespp marijkesluizen.pbes marijkesluizen.txtpbes && pbesiteration marijkesluizen.txtpbes -itext. Sample_pbesiteration.txt