Description
I list here some bugs I've noticed when trying to apply the symbolic (BDD) synthesis applied to some of the DES-Book Examples.
For simplicity reasons, I suggest to also document and edit the known issues on the wiki.
-
Chapter 4. Controllability. It contains a Plant and a Supervisor. It crashes with the following Exception:
Exception in thread "AWT-EventQueue-0" java.lang.NullPointerException
at org.supremica.automata.ExtendedAutomataIndexMap.getEventIndex(ExtendedAutomataIndexMap.java:243)
at org.supremica.automata.BDD.EFA.BDDExtendedAutomata.getEventIndex(BDDExtendedAutomata.java:1710)
at org.supremica.automata.BDD.EFA.BDDExtendedAutomaton.initialize(BDDExtendedAutomaton.java:209)
at org.supremica.automata.BDD.EFA.BDDExtendedAutomata.initialize(BDDExtendedAutomata.java:484)
at org.supremica.automata.BDD.EFA.BDDExtendedAutomata.(BDDExtendedAutomata.java:243)
at org.supremica.automata.BDD.EFA.BDDExtendedSynthesizer.(BDDExtendedSynthesizer.java:76)
at org.supremica.gui.ide.actions.EditorSynthesizerAction.doAction(EditorSynthesizerAction.java:185)
at org.supremica.gui.ide.actions.EditorSynthesizerAction.actionPerformed(EditorSynthesizerAction.java:115)
at javax.swing.AbstractButton.fireActionPerformed(Unknown Source)
This could simply be a known issue. -
Chapter 4 - Uncontrollable States. Besides the error with the verification tool mentionned in a comment to issue 115, the symbolic synthesis does not always return the same result.
Most of the time it returns two guards:
Guard Sp_curr != p1 with the term size 1 is generated for edge <q0, a1, q1> of automaton "P".
Guard Sp_curr != p1 with the term size 1 is generated for edge <q3, a1, q2> of automaton "P".
But, from time to time, it also completely forbids two other transitions:
Guard Sp_curr != p1 with the term size 1 is generated for edge <q0, a1, q1> of automaton "P".
Guard Sp_curr != p1 with the term size 1 is generated for edge <q3, a1, q2> of automaton "P".
Edge <q0, a2, q3> in automaton "P" is FORBIDDEN.
Edge <q1, a2, q2> in automaton "P" is FORBIDDEN.
This is more problematic.