Newly introduced error with EFSM / EFA guard generation

[JulienProvost]

A new bug has been introduced since July 30th on the EFSM / EFA handling after synthesis guard generation.
I've talked to Zhennan, who suggest this might come from the GUI rather than from the BDD or guard generation code.

You’ll find attached an example where the symbolic guards generation returns an error, as well as a working example from July 30th.
errors.zip

Here the console logs:

• In Supremica:
  Waters/Supremica IDE 2.4, built 06.09.2018 17:15:34 MESZ
  JVM:1.8.0_181, Free/Total/Max mem: 138/195/3625 MiB
  Number of used BDD variables: 85
  Synthesis completed after 162 milliseconds.
  The nonblocking and controllable supervisor consists of 34985 states.
  The guards were generated in 65 milliseconds.

• in the cmd console:
  Nonblocking and controllable states computed!
  Exception in thread "AWT-EventQueue-0" java.lang.NullPointerException
  at org.supremica.gui.ide.actions.EditorSynthesizerAction.doAction(EditorSynthesizerAction.java:249)
  at org.supremica.gui.ide.actions.EditorSynthesizerAction.actionPerformed(EditorSynthesizerAction.java:107)
  at javax.swing.AbstractButton.fireActionPerformed(Unknown Source)
  at javax.swing.AbstractButton$Handler.actionPerformed(Unknown Source)
  at javax.swing.DefaultButtonModel.fireActionPerformed(Unknown Source)
  at javax.swing.DefaultButtonModel.setPressed(Unknown Source)
  at javax.swing.AbstractButton.doClick(Unknown Source)
  at javax.swing.plaf.basic.BasicMenuItemUI.doClick(Unknown Source)
  at javax.swing.plaf.basic.BasicMenuItemUI$Handler.mouseReleased(Unknown Source)
  at java.awt.AWTEventMulticaster.mouseReleased(Unknown Source)
  at java.awt.Component.processMouseEvent(Unknown Source)
  at javax.swing.JComponent.processMouseEvent(Unknown Source)
  at java.awt.Component.processEvent(Unknown Source)
  at java.awt.Container.processEvent(Unknown Source)
  at java.awt.Component.dispatchEventImpl(Unknown Source)
  at java.awt.Container.dispatchEventImpl(Unknown Source)
  at java.awt.Component.dispatchEvent(Unknown Source)
  at java.awt.LightweightDispatcher.retargetMouseEvent(Unknown Source)
  at java.awt.LightweightDispatcher.processMouseEvent(Unknown Source)
  at java.awt.LightweightDispatcher.dispatchEvent(Unknown Source)
  at java.awt.Container.dispatchEventImpl(Unknown Source)
  at java.awt.Window.dispatchEventImpl(Unknown Source)
  at java.awt.Component.dispatchEvent(Unknown Source)
  at java.awt.EventQueue.dispatchEventImpl(Unknown Source)
  at java.awt.EventQueue.access$500(Unknown Source)
  at java.awt.EventQueue$3.run(Unknown Source)
  at java.awt.EventQueue$3.run(Unknown Source)
  at java.security.AccessController.doPrivileged(Native Method)
  at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(Unknown Source)
  at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(Unknown Source)
  at java.awt.EventQueue$4.run(Unknown Source)
  at java.awt.EventQueue$4.run(Unknown Source)
  at java.security.AccessController.doPrivileged(Native Method)
  at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(Unknown Source)
  at java.awt.EventQueue.dispatchEvent(Unknown Source)
  at java.awt.EventDispatchThread.pumpOneEventForFilters(Unknown Source)
  at java.awt.EventDispatchThread.pumpEventsForFilter(Unknown Source)
  at java.awt.EventDispatchThread.pumpEventsForHierarchy(Unknown Source)
  at java.awt.EventDispatchThread.pumpEvents(Unknown Source)
  at java.awt.EventDispatchThread.pumpEvents(Unknown Source)
  at java.awt.EventDispatchThread.run(Unknown Source)

[robimalik]

Can you please explain what we should do to reproduce this error?

[JulienProvost]

Open the file Portal2_V20_init.wmod and then click Analyze > Symbolic (BDD) synthesis > then tick the option Add guards to the model (the other options are the default ones: nonblocking and controllable; Monolithic (symbolic)).

Ticking or not the Use normalising EFSM compiler options in the Preferences doesn't change the result.

[robimalik]

Also, the option gui.analyzer -> Include Seamless Synthesis must selected.
And algorithms.bdd -> BDD Library has to be set to Java, otherwise a different error (issue #82) occurs.

But despite all efforts, I cannot reproduce the NullPointerException in EditorSynthesizerAction. I get similar output in the Supremica log, but the stderr only shows debug messages about the synthesis process. I am using the latest version from GitHub, commit 6b99bb7, compiled both on Linux and Windows.

[JulienProvost]

Seamless integration was selected by default.
Normally the BDD library set to Buddy is working. However, I tested back with Java without success.

We've just pulled the Git repository and compiled it with ant initialize both on Windows 7 and 10, with Java 1.8.
Unfortunately, both return the same error.

[JulienProvost]

Actually, the error occurs also without even ticking the option Add guards to the model

With the version from July 30th, the GUI correctly returns:
Number of used BDD variables: 85
Synthesis completed after 266 milliseconds.
The nonblocking and controllable supervisor consists of 34985 states.
The guards were generated in 74 milliseconds.
Guard ((Pcb2Spot == 0 & ((Pcb1Spot == 0 & ((PanelSpot == 0 & ((PickingPCB2FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB2_curr == S1)) | (PickingPCB2FromSeparator_curr == S0 & ((PickingPCB1FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB1_curr == S1)) | (PickingPCB1FromSeparator_curr == S0 & (PanelToScrap_curr == S0 | (PanelToScrap_curr == S1 & PCBTest2IfGood_curr == S8))))))) | (PanelSpot == 1 & ((PickingPCB2FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB2_curr == S1)) | (PickingPCB2FromSeparator_curr == S0 & ((PickingPCB1FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB1_curr == S1)) | PickingPCB1FromSeparator_curr == S0)))))) | (Pcb1Spot == 1 & ((PanelSpot == 0 & ((PickingPCB2FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB2_curr == S1)) | (PickingPCB2FromSeparator_curr == S0 & (PanelToScrap_curr == S0 | (PanelToScrap_curr == S1 & PCBTest2IfGood_curr == S8))))) | (PanelSpot == 1 & ((PickingPCB2FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB2_curr == S1)) | PickingPCB2FromSeparator_curr == S0)))))) | (Pcb2Spot == 1 & ((Pcb1Spot == 0 & ((PanelSpot == 0 & ((PickingPCB1FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB1_curr == S1)) | (PickingPCB1FromSeparator_curr == S0 & (PanelToScrap_curr == S0 | (PanelToScrap_curr == S1 & PCBTest2IfGood_curr == S8))))) | (PanelSpot == 1 & ((PickingPCB1FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB1_curr == S1)) | PickingPCB1FromSeparator_curr == S0)))) | (Pcb1Spot == 1 & ((PanelSpot == 0 & (PanelToScrap_curr == S0 | (PanelToScrap_curr == S1 & PCBTest2IfGood_curr == S8))) | (PanelSpot == 1 & ((PickingPCB2FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB2_curr == S1)) | (PickingPCB2FromSeparator_curr == S0 & ((PickingPCB1FromSeparator_curr == S1 & (PCBTest2IfGood_curr == S8 & State_PCB1_curr == S1)) | (PickingPCB1FromSeparator_curr == S0 & (PanelToScrap_curr == S0 | (PanelToScrap_curr == S1 & PCBTest2IfGood_curr == S8)))))))))))) with the term size 69 is generated for edge <S1, LC_PickTest2, S0> of automaton "OnlyPickWhenDoneTesting2".
Guard ((PCBTest1IfGood_curr == S9 & ((Pcb2Spot == 0 & ((Pcb1Spot == 0 & ((PanelSpot == 0 & (PickingPCB2FromSeparator_curr == S0 & (PickingPCB1FromSeparator_curr == S0 & PanelToScrap_curr == S0))) | (PanelSpot == 1 & (PickingPCB2FromSeparator_curr == S0 & PickingPCB1FromSeparator_curr == S0)))) | (Pcb1Spot == 1 & (PickingPCB2FromSeparator_curr == S0 & PanelToScrap_curr == S0)))) | (Pcb2Spot == 1 & (PickingPCB2FromSeparator_curr == S0 & (PickingPCB1FromSeparator_curr == S0 & PanelToScrap_curr == S0))))) | (PCBTest1IfGood_curr == S8 & ((Pcb2Spot == 0 & ((Pcb1Spot == 0 & ((PickingPCB2FromSeparator_curr == S1 & State_PCB2_curr == S1) | (PickingPCB2FromSeparator_curr == S0 & ((PickingPCB1FromSeparator_curr == S1 & State_PCB1_curr == S1) | PickingPCB1FromSeparator_curr == S0)))) | (Pcb1Spot == 1 & ((PickingPCB2FromSeparator_curr == S1 & State_PCB2_curr == S1) | PickingPCB2FromSeparator_curr == S0)))) | (Pcb2Spot == 1 & ((Pcb1Spot == 0 & ((PickingPCB1FromSeparator_curr == S1 & State_PCB1_curr == S1) | PickingPCB1FromSeparator_curr == S0)) | (Pcb1Spot == 1 & (PanelSpot == 0 | (PanelSpot == 1 & ((PickingPCB2FromSeparator_curr == S1 & State_PCB2_curr == S1) | (PickingPCB2FromSeparator_curr == S0 & ((PickingPCB1FromSeparator_curr == S1 & State_PCB1_curr == S1) | PickingPCB1FromSeparator_curr == S0))))))))))) with the term size 44 is generated for edge <S1, LC_PickTest1, S0> of automaton "OnlyPickWhenDoneTesting1".
Guard ((Pcb2Spot != 0 | ((PanelSpot != 0 | ((PickingPCB2FromSeparator_curr != S1 | (((State_PCB2_curr != S1 | State_PCB1_curr == S1) & State_PCB2_curr != S0) & (State_PCB2_curr != S2 | State_PCB1_curr == S2))) & (PickingPCB2FromSeparator_curr != S0 | (PanelToScrap_curr != S1 | State_PCB1_curr == S1)))) & (PanelSpot != 1 | (PickingPCB2FromSeparator_curr != S1 | (((State_PCB2_curr != S1 | State_PCB1_curr == S1) & State_PCB2_curr != S0) & (State_PCB2_curr != S2 | State_PCB1_curr == S2)))))) & (Pcb2Spot != 1 | ((PanelSpot != 0 | (PanelToScrap_curr != S1 | State_PCB1_curr == S1)) & (PanelSpot != 1 | ((PickingPCB2FromSeparator_curr != S1 | (((State_PCB2_curr != S1 | State_PCB1_curr == S1) & State_PCB2_curr != S0) & (State_PCB2_curr != S2 | State_PCB1_curr == S2))) & (PickingPCB2FromSeparator_curr != S0 | (PickingPCB1FromSeparator_curr != S0 | (PanelToScrap_curr != S1 | State_PCB1_curr == S1)))))))) with the term size 33 is generated for edge <S0, LC_PickPcb1, S1> of automaton "PickThenPlace".
Guard ((Pcb1Spot != 0 | ((PanelSpot != 0 | ((PickingPCB1FromSeparator_curr != S1 | (((State_PCB2_curr != S1 | State_PCB1_curr == S1) & State_PCB2_curr != S0) & (State_PCB2_curr != S2 | State_PCB1_curr == S2))) & (PickingPCB1FromSeparator_curr != S0 | (PanelToScrap_curr != S1 | State_PCB2_curr == S1)))) & (PanelSpot != 1 | (PickingPCB1FromSeparator_curr != S1 | (((State_PCB2_curr != S1 | State_PCB1_curr == S1) & State_PCB2_curr != S0) & (State_PCB2_curr != S2 | State_PCB1_curr == S2)))))) & (Pcb1Spot != 1 | ((PanelSpot != 0 | (PanelToScrap_curr != S1 | State_PCB2_curr == S1)) & (PanelSpot != 1 | (PickingPCB2FromSeparator_curr != S0 | ((PickingPCB1FromSeparator_curr != S1 | (((State_PCB2_curr != S1 | State_PCB1_curr == S1) & State_PCB2_curr != S0) & (State_PCB2_curr != S2 | State_PCB1_curr == S2))) & (PickingPCB1FromSeparator_curr != S0 | (PanelToScrap_curr != S1 | State_PCB2_curr == S1)))))))) with the term size 33 is generated for edge <S0, LC_PickPcb2, S1> of automaton "PickThenPlace".
Guard ((Pcb2Spot != 0 | ((Pcb1Spot != 0 | ((PickingPCB2FromSeparator_curr != S1 | State_PCB2_curr == S1) & (PickingPCB2FromSeparator_curr != S0 | (PickingPCB1FromSeparator_curr != S1 | State_PCB1_curr == S1)))) & (Pcb1Spot != 1 | (PickingPCB2FromSeparator_curr != S1 | State_PCB2_curr == S1)))) & (Pcb2Spot != 1 | ((Pcb1Spot != 0 | (PickingPCB1FromSeparator_curr != S1 | State_PCB1_curr == S1)) & (Pcb1Spot != 1 | ((PickingPCB2FromSeparator_curr != S1 | State_PCB2_curr == S1) & (PickingPCB2FromSeparator_curr != S0 | (PickingPCB1FromSeparator_curr != S1 | State_PCB1_curr == S1))))))) with the term size 20 is generated for edge <S0, LC_PickPanel, S1> of automaton "PickThenPlace".

[robimalik]

If I check "Print the computed guards", then I get this error.
In this case, it also happens with the "Stick Picking Game" from "Games and Puzzles" in the Example menu.
The error seems to occur in the guard generation process. On line 247 of EditorSynthesizerAction, some BDDExtendedGuardGenerator is null when it should not be. I have to disagree: this does not come from the GUI but from the BDD or guard generation code.

[JulienProvost]

Thank you Robi!

A few more details:
For my example Portal2_V20_init.wmod, if none of the options Print the computed guards and Add guards to the model and Save the result in a file then there is no error. But, I don't get any result either ;-(
For the Stick Picking Game, ticking Add guards to the model but not Print the computed guards does the job.

[Zhennan-Fei]

The error is indeed from the code that either prints guards or add them into the model.
The bug has been fixed.

However, when trying to synthesise the supervisor after adding the generated guards in the first example, another exception occurred. This has been also fixed but the solution needs to be improved.