Unexpected error when asking for witness on its-ctl CTL about itstools HOT 3 CLOSED

Hi,
sorry for the lag, it looks like a bug as there is no reason we lose events in the ETF scenario, I'll investigate and reproduce today and notify here if/when it's patched.

Some tips : for more readable traces you usually want to activate "-backward" as forward time operators are more efficient for solving but make for harder traces to read.

You might also consider using/generating a GAL input for your models, that is the currently recommended approach, we can then regenerate a PINS model from a GAL if you want to interact with LTSmin.

I'll post here when I4ve debugged you example.

from itstools.

So, your ETF files are unusual they use features that are not well supported such as action labels and a one-hot encoding for your automaton + no locality/a single transition group.
So this ETF input has mostly been used with models that came thru LTSmin from Divine models, the procedure to build traces actually has quite a bit of code to assign unlabeled transitions to a "process" a concept that exists in Divine but not really in ETF.

While I would be willing to improve our support for this type of ETF file, it would have to be because it is truly useful for you, but perhaps we can find another path to handle your models e.g. GAL.
trace.zip

here is a GAL file for this model + readable trace. Formula 3 is trivially false because initial state does not respect the condition.
I just wrote the file by looking at your PNG, then right-click -> Run As -> ITS-model check
Then right click again -> run as -> run configurations
Switch to its-ctl on the "model selection" tab and add witness and backward on "CTL" tab and run.

from itstools.

Hi Yann,
Thank you for the investigation. At this moment i can't justify to spend a lot of effort in improving this. :-).
The models that i am working on are not coming from Divine, nor LTSMIN. I only have an explicit model and i needed a way to encoded it for a model checker. That is why i was using ETF.

I will investigate the usability of the skeleton you provided to see i if can encode my explicit model in GAL. I also like the log with the trace: this is good to comprehend, better than the log from the etf version of the toy model.

Thank you.
Carlo

from itstools.