Merge 0da582c into 19a18bd

ci/flow-mpsat-g/test.result.ref

@@ -1 +1 @@
-24 out of 28 benchmarks passed the test
+22 out of 26 benchmarks passed the test

settings.gradle

@@ -22,7 +22,7 @@ gradle.ext.javaTargetVersion = JavaVersion.VERSION_11
 gradle.ext.javaReleaseVersion = 11  /* Must be integer, e.g. 11 for JDK11*/
 
 // Checkstyle code linter (https://checkstyle.sourceforge.io/)
-gradle.ext.checkstyleVersion = '10.12.2'
+gradle.ext.checkstyleVersion = '10.12.3'
 // PMD code analyser (https://pmd.github.io/)
 gradle.ext.pmdVersion = '6.55.0'
 // Jacoco code coverage (https://www.eclemma.org/jacoco/)

workcraft/MpsatVerificationPlugin/src/org/workcraft/plugins/mpsat_verification/gui/LocalSelfTriggeringDialog.java

@@ -6,7 +6,10 @@
 import org.workcraft.plugins.builtin.settings.SignalCommonSettings;
 import org.workcraft.plugins.mpsat_verification.presets.LocalSelfTriggeringDataPreserver;
 import org.workcraft.plugins.mpsat_verification.presets.LocalSelfTriggeringParameters;
+import org.workcraft.plugins.petri.Transition;
+import org.workcraft.plugins.petri.utils.PetriUtils;
 import org.workcraft.plugins.stg.Signal;
+import org.workcraft.plugins.stg.SignalTransition;
 import org.workcraft.plugins.stg.Stg;
 import org.workcraft.utils.GuiUtils;
 import org.workcraft.utils.SortUtils;
@@ -60,8 +63,8 @@ public void windowOpened(WindowEvent e) {
     public JPanel createContentPanel() {
         Stg stg = WorkspaceUtils.getAs(getUserData().getWorkspaceEntry(), Stg.class);
         localSignalList = new LocalSignalList(
-                stg.getSignalReferences(Signal.Type.OUTPUT),
-                stg.getSignalReferences(Signal.Type.INTERNAL));
+                getSyntacticSelfTriggeringSignals(stg, stg.getSignalReferences(Signal.Type.OUTPUT)),
+                getSyntacticSelfTriggeringSignals(stg, stg.getSignalReferences(Signal.Type.INTERNAL)));
 
         LocalSelfTriggeringParameters parameters = getUserData().loadData();
         Set<String> exceptionSignals = parameters.getExceptionSignals();
@@ -80,6 +83,25 @@ public JPanel createContentPanel() {
         return result;
     }
 
+    private Set<String> getSyntacticSelfTriggeringSignals(Stg stg, Collection<String> signals) {
+        Set<String> result = new HashSet<>();
+        for (String signal : signals) {
+            Collection<SignalTransition> signalTransitions = stg.getSignalTransitions(signal);
+            for (Transition signalTransition : signalTransitions) {
+                Collection<Transition> syntacticTriggerTransitions =
+                        PetriUtils.getSyntacticTriggerTransitions(stg, signalTransition);
+
+                syntacticTriggerTransitions.remove(signalTransition);
+                syntacticTriggerTransitions.retainAll(signalTransitions);
+                if (!syntacticTriggerTransitions.isEmpty()) {
+                    result.add(signal);
+                    break;
+                }
+            }
+        }
+        return result;
+    }
+
     private void selectSignals(LocalSignalList localSignalList, Set<String> signals) {
         ListModel<String> signalListModel = localSignalList.getModel();
         List<Integer> indices = new ArrayList<>();

workcraft/MpsatVerificationPlugin/src/org/workcraft/plugins/mpsat_verification/presets/DiInterfaceParameters.java

@@ -29,16 +29,17 @@ public class DiInterfaceParameters {
             "            SUSPECTS = gather ti_trig in pre pre_ti * TRINP \\ {ti} s.t.\n" +
             "                ~is_empty((post ti_trig \\ pre ti_trig) * pre_ti)\n" +
             "                &\n" +
-            "                ~exists set in EXCEPTIONS { S ti in set & S ti_trig in set } { ti_trig }\n" +
+            "                ~exists set in EXCEPTIONS { S ti in set & S ti_trig in set }\n" +
+            "            { ti_trig }\n" +
             "        {\n" +
             "            // Check if some ti_trig can trigger ti\n" +
             "            exists ti_trig in SUSPECTS {\n" +
-            "                forall p in pre_ti \\ post ti_trig { $p }\n" +
+            "                forall p in pre_ti \\ post ti_trig { $ p }\n" +
             "                &\n" +
-            "                @ti_trig\n" +
+            "                @ ti_trig\n" +
+            "                &\n" +
+            "                (S ti = S ti_trig ? ~@ ti : ~@S ti)\n" +
             "            }\n" +
-            "            &\n" +
-            "            ~@S ti\n" +
             "        }\n" +
             "    }\n" +
             "}\n";

workcraft/MpsatVerificationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/DeadlockFreenessOutputInterpreter.java

@@ -69,7 +69,7 @@ public List<Solution> processSolutions(List<Solution> solutions) {
             for (SignalTransition transition : stg.getSignalTransitions()) {
                 Signal.Type type = transition.getSignalType();
                 if (stg.isEnabled(transition) && (type == Signal.Type.OUTPUT)) {
-                    String signal = transition.getSignalName();
+                    String signal = stg.getSignalReference(transition);
                     LogUtils.logWarning("Deadlock trace is spurious because it leads to non-conformant output '" + signal + "'");
                     isConformantTrace = false;
                     break;

workcraft/MpsatVerificationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/DiInterfaceInterpreter.java

@@ -48,7 +48,7 @@ public List<Solution> processSolutions(List<Solution> solutions) {
             Set<String> nonDiInputSignals = getNonDiInputSignals(stg);
             if (!nonDiInputSignals.isEmpty()) {
                 String comment = TextUtils.wrapMessageWithItems(
-                        "Sensitive to delay input signal set", nonDiInputSignals);
+                        "Interface is sensitive to input delays in the set", nonDiInputSignals);
 
                 result.add(new Solution(trace, null, comment));
             }
@@ -61,18 +61,18 @@ private HashSet<String> getNonDiInputSignals(StgModel stg) {
         HashSet<String> result = new HashSet<>();
         HashSet<SignalTransition> enabledInputSignalTransitions = getEnabledInputSignalTransitions(stg);
         for (SignalTransition inputSignalTransition : enabledInputSignalTransitions) {
-            String signalName = inputSignalTransition.getSignalName();
+            String signal = stg.getSignalReference(inputSignalTransition);
             stg.fire(inputSignalTransition);
             HashSet<SignalTransition> newEnabledInputSignalTransitions = getEnabledInputSignalTransitions(stg);
             newEnabledInputSignalTransitions.removeAll(enabledInputSignalTransitions);
             stg.unFire(inputSignalTransition);
             // Check which newly enabled transitions are of input signal
             for (SignalTransition newEnabledLocalSignalTransition : newEnabledInputSignalTransitions) {
                 if (newEnabledLocalSignalTransition.getSignalType() == Signal.Type.INPUT) {
-                    Set<String> signalNames = new HashSet<>();
-                    signalNames.add(signalName);
-                    signalNames.add(newEnabledLocalSignalTransition.getSignalName());
-                    result.add("{" + String.join(", ", signalNames) + "}");
+                    Set<String> signals = new HashSet<>();
+                    signals.add(signal);
+                    signals.add(stg.getSignalReference(newEnabledLocalSignalTransition));
+                    result.add("{" + String.join(", ", signals) + "}");
                 }
             }
         }

workcraft/MpsatVerificationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/LocalSelfTriggeringInterpreter.java

@@ -61,15 +61,16 @@ private HashSet<String> getSelfTriggeringLocalSignals(StgModel stg) {
         HashSet<String> result = new HashSet<>();
         HashSet<SignalTransition> enabledLocalSignalTransitions = getEnabledLocalSignalTransitions(stg);
         for (SignalTransition localSignalTransition : enabledLocalSignalTransitions) {
-            String signalName = localSignalTransition.getSignalName();
+            String signal = stg.getSignalReference(localSignalTransition);
             stg.fire(localSignalTransition);
             HashSet<SignalTransition> newEnabledLocalSignalTransitions = getEnabledLocalSignalTransitions(stg);
             newEnabledLocalSignalTransitions.removeAll(enabledLocalSignalTransitions);
             stg.unFire(localSignalTransition);
             // Check which newly enabled transitions are of the fired signal
             for (SignalTransition newEnabledLocalSignalTransition : newEnabledLocalSignalTransitions) {
-                if (newEnabledLocalSignalTransition.getSignalName().equals(signalName)) {
-                    result.add(signalName);
+                String otherSignal = stg.getSignalReference(newEnabledLocalSignalTransition);
+                if (otherSignal.equals(signal)) {
+                    result.add(signal);
                 }
             }
         }

workcraft/MpsatVerificationPlugin/test-src/org/workcraft/plugins/mpsat_verification/VerificationCommandTests.java

@@ -216,20 +216,40 @@ void testToggleSignalVerification() throws DeserialisationException {
     }
 
     @Test
-    void testPulserVerification() throws DeserialisationException {
-        String workName = PackageUtils.getPackagePath(getClass(), "pulser.stg.work");
+    void testDlatchVerification() throws DeserialisationException {
+        String workName = PackageUtils.getPackagePath(getClass(), "dlatch.stg.work");
         testVerificationCommands(workName,
                 false, // combined
                 true,  // consistency
                 true,  // deadlock freeness
                 true,  // input properness
                 true,  // output persistency
                 true,  // output determinacy
-                false,  // CSC
-                false,  // USC
-                false,  // absence of self-triggering local signals
-                true,  // DI interface
-                false,  // normalcy
+                true, // CSC
+                true, // USC
+                true,  // absence of self-triggering local signals
+                false, // DI interface
+                false, // normalcy
+                null,  // mutex implementability (late protocol)
+                null   // mutex implementability (early protocol)
+        );
+    }
+
+    @Test
+    void testInoutPulseVerification() throws DeserialisationException {
+        String workName = PackageUtils.getPackagePath(getClass(), "inout_pulse.stg.work");
+        testVerificationCommands(workName,
+                false, // combined
+                true,  // consistency
+                true,  // deadlock freeness
+                true,  // input properness
+                true,  // output persistency
+                true,  // output determinacy
+                false, // CSC
+                false, // USC
+                false, // absence of self-triggering local signals
+                false, // DI interface
+                false, // normalcy
                 null,  // mutex implementability (late protocol)
                 null   // mutex implementability (early protocol)
         );
@@ -245,11 +265,11 @@ void testPulserSelfTriggerExceptionsVerification() throws DeserialisationExcepti
                 true,  // input properness
                 true,  // output persistency
                 true,  // output determinacy
-                false,  // CSC
-                false,  // USC
+                false, // CSC
+                false, // USC
                 true,  // absence of self-triggering local signals
                 true,  // DI interface
-                false,  // normalcy
+                false, // normalcy
                 null,  // mutex implementability (late protocol)
                 null   // mutex implementability (early protocol)
         );

workcraft/PetriPlugin/src/org/workcraft/plugins/petri/utils/PetriUtils.java

@@ -13,6 +13,7 @@
 import org.workcraft.utils.LogUtils;
 import org.workcraft.utils.TextUtils;
 
+import java.util.Collection;
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Set;
@@ -142,4 +143,13 @@ public static void removeIsolatedMarkedVisualPlaces(VisualModel visualModel) {
         }
     }
 
+    public static Collection<Transition> getSyntacticTriggerTransitions(PetriModel model, Transition transition) {
+        Set<Transition> result = new HashSet<>();
+        Set<Place> predPlaces = model.getPreset(transition, Place.class);
+        for (Place predPlace : predPlaces) {
+            result.addAll(model.getPreset(predPlace, Transition.class));
+        }
+        return result;
+    }
+
 }

workcraft/StgPlugin/src/org/workcraft/plugins/stg/VisualSignalTransition.java

@@ -26,7 +26,7 @@ public String getName() {
         if (signalName == null) {
             signalName = "";
         }
-        final StringBuffer result = new StringBuffer(signalName);
+        final StringBuilder result = new StringBuilder(signalName);
         switch (getReferencedComponent().getDirection()) {
         case PLUS:
             result.append("+");