search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
51 stars 30 forks source link

Add a HOA format input that accepts (the negation) of a language #202

Closed yanntm closed 2 years ago

yanntm commented 2 years ago

As discussed with @alaarman and with the help of @etienne-renault and @adl this PR adds a --hoa flag to ltsmin.

It's been tested and debugged with the MCC benchmark so it seems clean semantically This is with the flags I use, which do include POR I spent more testing on --buchi-type=spotbuchi than =tgba but both work with state based AP at least.

The PR includes Alfons's patch for "weak" detection so it closes https://github.com/utwente-fmt/ltsmin/issues/201

I can add tests but mine are all .c/.so inputs to pins2lts-mc there is no model for a test setup like that (at least in what I saw) and I'm unsure how many you'd like. But I have plenty of test cases maybe I send one set of files + formula + verdict and if you set it up as an example test Alfons so I can see the files I need to add/edit, and I'll generate as many as you like.

Some hacking of strings used as keys which did not have homogeneous whitespace was also added in the AP registration phase, I hope we didn't break anything for other input languages/AP.

Please don't hesitate to comment or ask for changes we tried to not too intrusive but registering AP was a bit of a pain, we end up parsing a textual formula that is the AND of all AP just to get them registered.

yanntm commented 2 years ago

as an example set of test files/formulas, we have those I attached to the Issue #201