search

reactive-systems / MCHyper

A hardware model checker for hyperproperties
GNU Affero General Public License v3.0
18 stars 1 forks source link

No model provided #2

Open DonCyriac opened 3 years ago

DonCyriac commented 3 years ago

Hi, I was trying to make the tool work for some time. But it seems like there is something I am missing. I made a simple robot FSM

robot.txt

(non-deterministic) using NuSMV and converted it to an aag file using smvflatten and smvtoaig tool from the aiger suite. The robot model is working fine in NuSMV, including the flattened model. The flattened model has a huge number of states when I try the pick_state command in NuSMV with it, but I still can check the model using the check_ltlspec command. When I try and put the aag file in the tool, it does not produce a model. I tried doing the same with an SMV model synthesized by your own tool BoSy and it works. Please help me with this. Do I need to do something differently or is this a scaling issue that I can solve by making my FSM more deterministic?

NorineCoenen commented 3 years ago

Hi, can you provide a minimal working example (Aiger file and MCHyper call) producing the error you encounter?

DonCyriac commented 3 years ago

Hi, I think I have got around that problem somehow. But I have a few other doubts is it ok if I post my questions here?