search

reactive-systems / syfco

Synthesis Format Conversion Tool
MIT License
23 stars 12 forks source link

Add SMV as a format target option #16

Closed ltentrup closed 8 years ago

ltentrup commented 8 years ago

This enables the usage of the tool smvtoaig from the AIGER toolset to generate a monitoring automaton from a TLSF specification (which can be further used to model check solutions from TLSF synthesizer).

johnyf commented 8 years ago

A note about model checking with NuSMV as an alternative: I have used aigtosmv from the AIGER tools to convert the synthesized circuits to SMV, and then model checked them with NuSMV. In order to do so, I had to modify slightly the aigtosmv source code, to make it name the outputs within SMV as in the symbol table, instead of the "o#" that it uses otherwise.

This may provide an alternative in cases that there is an issue with another model checker.