Add SMV format with decomposed formulas

reactive-systems / syfco

Synthesis Format Conversion Tool

MIT License

23 stars 12 forks source link

Add SMV format with decomposed formulas #31

Closed meyerphi closed 4 years ago

meyerphi commented 4 years ago

This adds the format smv-decomp that outputs an SMV module file with several LTL formulas, obtained from splitting the specification at top-level conjunctions. This allows further compositional model checking based on the SMV file.

Some of the code is similiar to the changes proposed in #30, so if both will be merged one could possibly refactor out shared code.

gaperez64 commented 4 years ago

I am thinking... if we keep making ad-hoc compositional versions of all the supported formats, maybe we should factor this out as an option that syfco gives for all formats?