search

gaperez64 / acacia-bonsai

A minimal implementation of reactive synthesis via universal co-Buchi automata using antichains
GNU General Public License v3.0
4 stars 3 forks source link

Model checking not passing for synthesized controller ltl2dba_U18.tlsf #33

Closed gaperez64 closed 1 year ago

gaperez64 commented 1 year ago

See title, and benchmarks repo from SYNTCOMP

gaperez64 commented 1 year ago

Here is a log with the debug prints from acacia when solving that benchmark. Also, for information, if the parameter n is changed to any value smaller than 17 then the model checker agrees that the synthesized controller is correct. For 17 and 18 it says it finds a counterexample. log.zip

gaperez64 commented 1 year ago

I think a good first step is to check, based on the log above, that the synthesized controller (as represented internally) has the property of being inductive (so it stays within the set of states it considers reachable) and complete (so for every valuation of the inputs, there is a transition). If this is the case then it narrows down the bug to: 1. the set of states not all being safe or 2. the encoding of the controller into a BDD and subsequently into AIGER or 3. the dynamics of the controller not matching those of the original automaton.

gaperez64 commented 1 year ago

Update: the solution being inductive is indeed true. However, completeness cannot be guaranteed since we never ask spot to produce complete automata (duh!). I have now changed a few BDD-based instructions (quantification operations) and things seem to behave better now.

In short: I believe buddy does not like to be given a BDD representing a set without an explicit pointer to it. For instance, quantifying the conjunction of inputs and outputs creates a new BDD passed to the quantification function/procedure while the caller has no variable/reference to that BDD. After giving it only BDDs with references, all weird things went away. Granted, I cannot say exactly what the reason of the bug was :)

For now, I'm closing the issue as I cannot reproduce it anymore.

gaperez64 commented 1 year ago

NOPE: StarExec still exhibits the bug with ltl2dba_U18. I'll have to try to reproduce it locally

gaperez64 commented 1 year ago

Maybe, bdd_forall was broken in Spot's buddy. Additionally, I believe that the way in which BDDs were stored for the AIGER dump was not safe if some garbage-collection or reordering was triggered. I have now referenced all bdds whose id we kept track of, just so that they are not cleaned in the next GC run. It seems to work, but model checking times out now...