From 38ea76b6ef2e154935cf9ba4508ecdb6ea3f0e9e Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Thu, 4 Aug 2016 15:38:32 +0000
Subject: [PATCH] Update on random management in avatar modelc checker
---
src/avatartranslator/AvatarRandom.java | 15 ++++++++++-----
src/avatartranslator/AvatarStateMachine.java | 4 ++--
src/avatartranslator/AvatarTransition.java | 4 +++-
.../modelchecker/AvatarModelChecker.java | 7 ++++---
4 files changed, 19 insertions(+), 11 deletions(-)
diff --git a/src/avatartranslator/AvatarRandom.java b/src/avatartranslator/AvatarRandom.java
index 666afb4e8f..04972ce13a 100644
--- a/src/avatartranslator/AvatarRandom.java
+++ b/src/avatartranslator/AvatarRandom.java
@@ -87,11 +87,6 @@ public class AvatarRandom extends AvatarStateMachineElement {
functionId = _functionId;
}
- public AvatarStateMachineElement basicCloneMe(AvatarStateMachineOwner _block) {
- AvatarRandom ar = new AvatarRandom(getName(), getReferenceObject());
- return ar;
- }
-
public String getNiceName() {
return "Random between " + minValue + " and " + maxValue + " stored in " + variable;
}
@@ -99,4 +94,14 @@ public class AvatarRandom extends AvatarStateMachineElement {
public void translate (AvatarTranslator translator, Object arg) {
translator.translateRandom (this, arg);
}
+
+ public AvatarStateMachineElement basicCloneMe(AvatarStateMachineOwner _block) {
+ AvatarRandom ar = new AvatarRandom(getName() + "_clone", getReferenceObject());
+
+ ar.setVariable(variable);
+ ar.setValues(minValue, maxValue);
+ ar.setFunctionId(functionId);
+
+ return ar;
+ }
}
diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index 8dff4ce2a8..dfce91d279 100644
--- a/src/avatartranslator/AvatarStateMachine.java
+++ b/src/avatartranslator/AvatarStateMachine.java
@@ -378,8 +378,8 @@ private void addStatesToTransitionsBetweenTwoNonStates(AvatarBlock _block) {
AvatarState randomState = new AvatarState("StateForRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
AvatarState beforeRandom = new AvatarState("StateBeforeRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
AvatarTransition at2 = new AvatarTransition(_block, "Transition2ForRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
- at2.addGuard("[" + random.getVariable() + " < " + random.getMaxValue() + "]");
- at2.addAction(random.getVariable() + "=" + random.getVariable() + "1");
+ at2.setGuard("[" + random.getVariable() + " < " + random.getMaxValue() + "]");
+ at2.addAction(random.getVariable() + "=" + random.getVariable() + " + 1");
// Adding elements
toAdd.add(at1);
diff --git a/src/avatartranslator/AvatarTransition.java b/src/avatartranslator/AvatarTransition.java
index daff92d7bc..623ee24bd9 100644
--- a/src/avatartranslator/AvatarTransition.java
+++ b/src/avatartranslator/AvatarTransition.java
@@ -90,10 +90,12 @@ public class AvatarTransition extends AvatarStateMachineElement {
public void setGuard (String _guard) {
this.guard = AvatarGuard.createFromString (this.block, _guard);
+ TraceManager.addDev("Setting guard = " + guard);
}
public void addGuard(String _g) {
AvatarGuard guard = AvatarGuard.createFromString (this.block, _g);
+ TraceManager.addDev("Adding guard = " + guard);
this.guard = AvatarGuard.addGuard (this.guard, guard, "and");
}
@@ -194,7 +196,7 @@ public class AvatarTransition extends AvatarStateMachineElement {
public void addAction(String _action) {
AvatarAction aa = AvatarTerm.createActionFromString (block, _action);
- TraceManager.addDev("Avatar action = " + aa);
+ TraceManager.addDev("Avatar action : " + aa);
if (aa != null)
actions.add(aa);
}
diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index 347949f82d..ec3712b40e 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -100,7 +100,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (_spec != null) {
initialSpec = _spec;
//TraceManager.addDev("Before clone:\n" + spec);
- //spec = _spec.advancedClone();
+ spec = initialSpec.advancedClone();
//TraceManager.addDev("After clone:\n" + spec);
}
ignoreEmptyTransitions = true;
@@ -123,6 +123,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
public int getNbOfStates() {
+ if (states == null) {
+ return 0;
+ }
return states.size();
}
@@ -244,8 +247,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (spec == null) {
return;
}
-
- spec = initialSpec.advancedClone();
stoppedBeforeEnd = false;
stateID = 0;
--
GitLab