From 60bacf6a23c03e205cd8c986b73475295f2bc177 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Thu, 7 Apr 2022 17:37:53 +0200
Subject: [PATCH] Reversing to previous model-checker
---
.../modelchecker/AvatarModelChecker.java | 25 +++----------------
.../test/java/cli/CLIDiploToAvatarTest.java | 6 +++--
2 files changed, 8 insertions(+), 23 deletions(-)
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 04e22cf495..7f8406c86e 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -1184,8 +1184,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
for (AvatarStateMachineElement elt : ase.getNexts()) {
if (elt instanceof AvatarTransition) {
- handleAvatarTransition((AvatarTransition) elt, block, sb, cpt, transitions,
- ase.getNexts().size() > 1);
+ handleAvatarTransition((AvatarTransition) elt, block, sb, cpt, transitions, ase.getNexts().size() > 1);
}
}
@@ -1224,10 +1223,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
SpecificationTransition st = null;
// See whether there is at least one transition with an immediate internal action with no alternative in the same block
for (SpecificationTransition tr : transitions) {
- if ((AvatarTransition.isActionType(tr.getType()) && (tr.clockMin == tr.clockMax) && (tr.clockMin == 0)) ||
- tr.getType() == AvatarTransition.TYPE_EMPTY) {
+ if ((AvatarTransition.isActionType(tr.getType()) && (tr.clockMin == tr.clockMax) && (tr.clockMin == 0)) || tr.getType() == AvatarTransition.TYPE_EMPTY) {
// Must look for possible transitions from the same state
- if (!(tr.fromStateWithMoreThanOneTransition) /*|| onlyOnetimeSameBlockTransition(tr, transitions)*/) {
+ if (!(tr.fromStateWithMoreThanOneTransition)) {
st = tr;
if (ignoreInternalStates) { // New behavior
computeAllInternalStatesFrom(_ss, st);
@@ -1389,20 +1387,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
mustStop();
}
- private boolean onlyOnetimeSameBlockTransition(SpecificationTransition st, ArrayList<SpecificationTransition> transitions ) {
-
- AvatarStateMachineOwner block = st.transitions[0].getBlock();
- for(SpecificationTransition specTr: transitions) {
- if (specTr != st) {
- if (specTr.transitions[0].getBlock() == block) {
- //TraceManager.addDev("Return false in onlyOnetimeSameBlockTransition");
- return false;
- }
- }
- }
- //TraceManager.addDev("Return true in onlyOnetimeSameBlockTransition");
- return true;
- }
private void computeAllInternalStatesFrom(SpecificationState _ss, SpecificationTransition st) {
SpecificationState newState = _ss.advancedClone();
@@ -1702,8 +1686,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//return evaluateBoolExpression(s, _block, _sb);
}
- private void handleAvatarTransition(AvatarTransition _at, AvatarBlock _block, SpecificationBlock _sb, int _indexOfBlock,
- ArrayList<SpecificationTransition> _transitionsToAdd, boolean _fromStateWithMoreThanOneTransition) {
+ private void handleAvatarTransition(AvatarTransition _at, AvatarBlock _block, SpecificationBlock _sb, int _indexOfBlock, ArrayList<SpecificationTransition> _transitionsToAdd, boolean _fromStateWithMoreThanOneTransition) {
if (_at.type == AvatarTransition.UNDEFINED) {
return;
}
diff --git a/ttool/src/test/java/cli/CLIDiploToAvatarTest.java b/ttool/src/test/java/cli/CLIDiploToAvatarTest.java
index 2fd131f85d..25e9aee45f 100644
--- a/ttool/src/test/java/cli/CLIDiploToAvatarTest.java
+++ b/ttool/src/test/java/cli/CLIDiploToAvatarTest.java
@@ -63,9 +63,10 @@ public class CLIDiploToAvatarTest extends AbstractTest implements InterpreterOut
private final static String PATH_TO_EXPECTED_FILE = "cli/expected/";
private StringBuilder outputResult;
- private final int[] statesInfo = {430, 102, 102};
+ private final int[] statesInfo = {5285, 350, 350};
+ private final int[] transitionsInfo = {13903, 649, 649};
+
private final int[] statesMinimizeInfo = {63, 21, 21};
- private final int[] transitionsInfo = {499, 111, 111};
private final int[] transitionsMinimizeInfo = {132, 30, 30};
@@ -123,6 +124,7 @@ public class CLIDiploToAvatarTest extends AbstractTest implements InterpreterOut
System.out.println("i=" + i + "/ RG states=" + graph.getNbOfStates() + " transitions=" + graph.getNbOfTransitions());
+
assertTrue(graph.getNbOfStates() == statesInfo[i]);
assertTrue(graph.getNbOfTransitions() == transitionsInfo[i]);
--
GitLab