Merge branch 'bugfix/controlled-det-goal-checks' into 'master'

Reject controllerSpec clauses other than controllable/safety with controlled_det

See merge request !17

maven-root/mtsa/src/main/java/ltsa/lts/CompositionExpression.java

@@ -364,6 +364,9 @@ public class CompositionExpression {
 
         ControllerGoalDefinition pendingGoal = ControllerGoalDefinition
                 .getDefinition(goal);
+        if (c.isControlledDet) {
+            checkControlledDetGoal(pendingGoal);
+        }
         c.env = c.machines.get(0);
         c.machines.addAll(CompositionExpression.preProcessSafetyReqs(
                 pendingGoal, output));
@@ -371,6 +374,68 @@ public class CompositionExpression {
                 pendingGoal);
     }
 
+    /**
+     * A {@code controlled_det} composition drives its determinisation purely from the
+     * {@code controllable} clause of its {@code controllerSpec}: the controllable determinisation
+     * reads {@code goal.getControllableActions()} and nothing else (see
+     * {@link TransitionSystemDispatcher#makeControlledDeterminisation}). The {@code safety} clause
+     * is also honoured, because its property is composed into the model before determinisation
+     * (see {@link #preProcessSafetyReqs}). Every other clause (liveness, assumption, reachability,
+     * nonblocking, ...) would be silently ignored, which is misleading, so reject it here.
+     */
+    private static void checkControlledDetGoal(ControllerGoalDefinition goalDef) {
+        List<String> extraClauses = new ArrayList<String>();
+        if (!goalDef.getGuaranteeDefinitions().isEmpty()) {
+            extraClauses.add("liveness");
+        }
+        if (!goalDef.getAssumeDefinitions().isEmpty()) {
+            extraClauses.add("assumption");
+        }
+        if (!goalDef.getFaultsDefinitions().isEmpty()) {
+            extraClauses.add("fault");
+        }
+        if (!goalDef.getBuchiDefinitions().isEmpty()) {
+            extraClauses.add("buchi");
+        }
+        if (!goalDef.getConcurrencyDefinitions().isEmpty()) {
+            extraClauses.add("concurrency");
+        }
+        if (!goalDef.getActivityDefinitions().isEmpty()) {
+            extraClauses.add("activity");
+        }
+        if (goalDef.getMarkingDefinitions() != null && !goalDef.getMarkingDefinitions().isEmpty()) {
+            extraClauses.add("marking");
+        }
+        if (goalDef.getDisturbanceActions() != null && !goalDef.getDisturbanceActions().isEmpty()) {
+            extraClauses.add("disturbance");
+        }
+        if (goalDef.isReachability()) {
+            extraClauses.add("reachability");
+        }
+        if (goalDef.isNonBlocking()) {
+            extraClauses.add("nonblocking");
+        }
+        if (goalDef.isPermissive()) {
+            extraClauses.add("permissive");
+        }
+        if (goalDef.isExceptionHandling()) {
+            extraClauses.add("exceptionHandling");
+        }
+        if (goalDef.isNonTransient()) {
+            extraClauses.add("nonTransient");
+        }
+        if (goalDef.isTestLatency()) {
+            extraClauses.add("testLatency");
+        }
+        if (goalDef.getLazyness() != null && goalDef.getLazyness() != 0) {
+            extraClauses.add("lazyness");
+        }
+        if (!extraClauses.isEmpty()) {
+            Diagnostics.fatal("controlled_det only supports the 'controllable' and 'safety' clauses "
+                    + "in its controllerSpec; remove: " + extraClauses + ".");
+        }
+    }
+
     public static Collection<CompactState> preProcessSafetyReqs(
             ControllerGoalDefinition goal, LTSOutput output) {
         ControllerGoalDefinition pendingGoal = ControllerGoalDefinition

maven-root/mtsa/src/test/java/MTSATests/controller/ControlledDetGoalTest.java

+package MTSATests.controller;
+
+import FSP2MTS.ac.ic.doc.mtstools.test.util.TestLTSOuput;
+import ltsa.dispatcher.TransitionSystemDispatcher;
+import ltsa.lts.CompositeState;
+import ltsa.lts.LTSCompiler;
+import ltsa.lts.LTSException;
+import ltsa.lts.LTSInputString;
+import org.junit.Test;
+
+import static org.junit.Assert.assertNotNull;
+import static org.junit.Assert.assertTrue;
+import static org.junit.Assert.fail;
+
+/**
+ * Verifies that a {@code controlled_det} composition rejects a {@code controllerSpec} that
+ * carries any clause other than {@code controllable} or {@code safety}. The controllable
+ * determinisation reads only {@code goal.getControllableActions()} (see
+ * {@link TransitionSystemDispatcher#makeControlledDeterminisation}), and {@code safety} is honoured
+ * because its property is composed into the model beforehand; every other clause ({@code liveness},
+ * {@code assumption}, {@code reachability}, {@code nonblocking}, ...) would be silently ignored. The
+ * guard lives in {@code CompositionExpression.checkControlledDetGoal} and aborts via
+ * {@code Diagnostics.fatal(...)} (which throws {@link LTSException}).
+ */
+public class ControlledDetGoalTest {
+
+    /** A non-deterministic model (M has two c1 transitions) so determinisation is meaningful. */
+    private static final String COMMON_MODEL =
+            "set Controllable = {c1, c2, c3}\n" +
+            "M = (c1 -> C2 | c1 -> C1),\n" +
+            "C1 = (c1 -> M | c2 -> C2 | c3 -> STOP),\n" +
+            "C2 = (c2 -> M | c1 -> C1 | c3 -> STOP).\n" +
+            "fluent F_C1 = <c1, Controllable\\{c1}>\n" +
+            "fluent F_C2 = <c2, Controllable\\{c2}>\n" +
+            "assert C1o2oU1 = (F_C1 || F_C2)\n";
+
+    /** controlled_det + a liveness clause -> rejected. */
+    private static final String FSP_CONTROLLED_DET_WITH_LIVENESS =
+            COMMON_MODEL +
+            "controlled_det ||DET = M~{G}.\n" +
+            "controllerSpec G = {\n" +
+            "    liveness = {C1o2oU1}\n" +
+            "    controllable = {Controllable}\n" +
+            "}\n";
+
+    /** controlled_det + only the controllable clause -> allowed (guard must not over-fire). */
+    private static final String FSP_CONTROLLED_DET_ONLY_CONTROLLABLE =
+            COMMON_MODEL +
+            "controlled_det ||DET = M~{G}.\n" +
+            "controllerSpec G = {\n" +
+            "    controllable = {Controllable}\n" +
+            "}\n";
+
+    @Test
+    public void controlledDetWithExtraClauseIsRejected() throws Exception {
+        TestLTSOuput output = new TestLTSOuput();
+        LTSCompiler compiler = new LTSCompiler(new LTSInputString(FSP_CONTROLLED_DET_WITH_LIVENESS), output, ".");
+        compiler.compile();
+        try {
+            CompositeState c = compiler.continueCompilation("DET");
+            TransitionSystemDispatcher.applyComposition(c, output);
+            fail("Expected LTSException for controlled_det with a non-controllable clause");
+        } catch (LTSException e) {
+            assertTrue("Unexpected rejection message: " + e.getMessage(),
+                    e.getMessage() != null
+                            && e.getMessage().contains("only supports the 'controllable' and 'safety'"));
+        }
+    }
+
+    /**
+     * The guard must not over-fire: a {@code controlled_det} spec that declares only the
+     * {@code controllable} clause must compile and determinise without the rejection.
+     */
+    @Test
+    public void controlledDetWithOnlyControllableIsNotRejectedByGuard() throws Exception {
+        TestLTSOuput output = new TestLTSOuput();
+        LTSCompiler compiler = new LTSCompiler(new LTSInputString(FSP_CONTROLLED_DET_ONLY_CONTROLLABLE), output, ".");
+        compiler.compile();
+        CompositeState c = compiler.continueCompilation("DET");
+        assertNotNull(c);
+        TransitionSystemDispatcher.applyComposition(c, output);
+    }
+}

maven-root/mtsa/src/test/resources/Alphabet/2013-controlleddet2.lts

@@ -28,6 +28,5 @@ controlled_det ||C = ENV~{G}.
 
 controllerSpec G = {
 	safety = {NOPS}
-    liveness = {PRESSED}
     controllable = {Controllable}
 }

maven-root/mtsa/src/test/resources/ControlledDeterminisationTests/controlled-det-1.lts

@@ -4,15 +4,8 @@ M = (c1->C2 | c1->C1),
 C1 = (c1->M | c2->C2 | c3->STOP),
 C2 = (c2->M | c1->C1 | c3->STOP).
 
-fluent F_C1 = <c1, Controllable\{c1}>
-fluent F_C2 = <c2, Controllable\{c2}>
-
-assert C1o2oU1 = (F_C1 || F_C2)
 controlled_det ||DET = M~{G}.
 
 controllerSpec G = {
-    liveness = {C1o2oU1}
-//	nonblocking
     controllable = {Controllable}
 }
-

maven-root/mtsa/src/test/resources/FSP/2013-controlleddet-example.lts

@@ -19,7 +19,6 @@ controlled_det ||DET = ENV~{G}.
 ||SOL = (E_C || ENV).
 
 controllerSpec G = {
-    liveness = {NorS}
     controllable = {Controllable}
 }
 

maven-root/mtsa/src/test/resources/FSP/2013-controlleddet2.lts

@@ -36,7 +36,6 @@ plant ||Plant = ENV~{G}.
 
 controllerSpec G = {
 //	safety = {NOPS}
-    liveness = {PRESSED}
     controllable = {Controllable}
 }
 

maven-root/mtsa/src/test/resources/FSP/2013-fse-robot-legal-env.lts

@@ -27,7 +27,6 @@ controller ||C = ENV~{G}.
 minimal ||Min_Controller = C.
 
 controllerSpec G = {
-    liveness = {PRESSED, EAST}
 //	nonblocking
     controllable = {Controllable}
 }

maven-root/mtsa/src/test/resources/FSP/2013-fse-robot-nb-env.lts

@@ -26,7 +26,5 @@ minimal ||Min_Controller = C.
 controlled_det ||DET = ENV~{G}.
 
 controllerSpec G = {
-    liveness = {PRESSED, EAST}
-	nonblocking
     controllable = {Controllable}
 }

maven-root/mtsa/src/test/resources/FSP/controlled-det-1.lts

@@ -11,7 +11,6 @@ assert C1o2oU1 = (F_C1 || F_C2)
 controlled_det ||DET = M~{G}.
 
 controllerSpec G = {
-    liveness = {C1o2oU1}
 //	nonblocking
     controllable = {Controllable}
 }