No model provided

[DonCyriac]

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]

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

[DonCyriac]

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?