From 39d993c629176c2d624bbab0e51752bce8d6b00f Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Mon, 6 Jun 2016 18:38:43 +0000
Subject: [PATCH] Update on model-checker
---
.../modelchecker/AvatarModelChecker.java | 27 +++++++++++++++----
.../modelchecker/SpecificationBlock.java | 6 +++++
.../modelchecker/SpecificationState.java | 13 ++++++---
.../modelchecker/SpecificationTransition.java | 20 ++++++++++++++
4 files changed, 58 insertions(+), 8 deletions(-)
diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index e598f5ede6..f696d45057 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -53,7 +53,7 @@ import avatartranslator.*;
import myutil.*;
public class AvatarModelChecker implements Runnable {
- private final static int DEFAULT_NB_OF_THREADS = 8;
+ private final static int DEFAULT_NB_OF_THREADS = 1;
private final static int SLEEP_DURATION = 500;
private AvatarSpecification spec;
@@ -309,11 +309,23 @@ public class AvatarModelChecker implements Runnable {
if (ignoreConcurrenceBetweenInternalActions) {
SpecificationTransition st = null;
- // See whether there is at least one transition with an internal action
+ // 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.getType() == AvatarTransition.TYPE_EMPTY) {
- st = tr;
- break;
+ if ((AvatarTransition.isActionType(tr.getType()) && (tr.clockMax == clockMin))|| tr.getType() == AvatarTransition.TYPE_EMPTY) {
+ // Must look for similar transitions in the the same block
+ boolean foundSameBlock = false;
+ for(SpecificationTransition tro: transitions) {
+ if (tro != tr) {
+ if (tro.hasBlockOf(tr)) {
+ foundSameBlock = true;
+ break;
+ }
+ }
+ }
+ if (!foundSameBlock) {
+ st = tr;
+ break;
+ }
}
}
if (st != null) {
@@ -322,12 +334,17 @@ public class AvatarModelChecker implements Runnable {
}
}
+ TraceManager.addDev("Possible transitions 4:" + transitions.size());
// For each realizable transition
// Make it, reset clock of the involved blocks to 0, increase clockmin/clockhmax of each block
// compute new state, and compare with existing ones
// If not a new state, create the link rom the previous state to the new one
// Otherwise create the new state and its link, and add it to the pending list of states
+ int cptt = 0;
for(SpecificationTransition tr: transitions) {
+ TraceManager.addDev("Handling transitions #" + cptt + " type =" + tr.getType());
+ cptt ++;
+
// Make tr
// to do so, must create a new state
SpecificationState newState = _ss.advancedClone();
diff --git a/src/avatartranslator/modelchecker/SpecificationBlock.java b/src/avatartranslator/modelchecker/SpecificationBlock.java
index 89d882bd92..5f6b8e4974 100644
--- a/src/avatartranslator/modelchecker/SpecificationBlock.java
+++ b/src/avatartranslator/modelchecker/SpecificationBlock.java
@@ -62,6 +62,8 @@ public class SpecificationBlock {
public static final int ATTR_INDEX = 3;
public int [] values; // state in block, clockmin, clockmax, variables
+ public boolean hasTimedTransition;
+ public boolean timeElapsed;
public SpecificationBlock() {
}
@@ -106,4 +108,8 @@ public class SpecificationBlock {
sb.values = values.clone();
return sb;
}
+
+ public boolean hasTimedTransition() {
+ return true;
+ }
}
diff --git a/src/avatartranslator/modelchecker/SpecificationState.java b/src/avatartranslator/modelchecker/SpecificationState.java
index daa93cb327..1425e6e986 100644
--- a/src/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/avatartranslator/modelchecker/SpecificationState.java
@@ -120,14 +120,21 @@ public class SpecificationState {
}
// Increase the clock of the blocks not in the transition
- // and puts the one of others to 0
+ // and having a timed transition.
+ // Otherwise, puts the one of others to 0
public void increaseClockOfBlocksExcept(SpecificationTransition _st) {
SpecificationBlock sb;
for(int i=0; i<blocks.length; i++) {
sb = blocks[i];
if (!(_st.hasBlockIndex(i))) {
- sb.values[SpecificationBlock.CLOCKMIN_INDEX] += _st.clockMin;
- sb.values[SpecificationBlock.CLOCKMAX_INDEX] += _st.clockMax;
+ if (sb.hasTimedTransition()) {
+ sb.values[SpecificationBlock.CLOCKMIN_INDEX] += _st.clockMin;
+ sb.values[SpecificationBlock.CLOCKMAX_INDEX] += _st.clockMax;
+ }
+ /*else {
+ sb.values[SpecificationBlock.CLOCKMIN_INDEX] = 0;
+ sb.values[SpecificationBlock.CLOCKMAX_INDEX] = 0;
+ }*/
} else {
sb.values[SpecificationBlock.CLOCKMIN_INDEX] = 0;
sb.values[SpecificationBlock.CLOCKMAX_INDEX] = 0;
diff --git a/src/avatartranslator/modelchecker/SpecificationTransition.java b/src/avatartranslator/modelchecker/SpecificationTransition.java
index a103472f85..3af6d35fc2 100644
--- a/src/avatartranslator/modelchecker/SpecificationTransition.java
+++ b/src/avatartranslator/modelchecker/SpecificationTransition.java
@@ -110,6 +110,26 @@ public class SpecificationTransition {
}
+ public boolean hasBlockOf(SpecificationTransition _tr) {
+ if (blocks == null) {
+ return false;
+ }
+
+ if (_tr.blocks == null) {
+ return false;
+ }
+
+ for (int i=0; i<blocks.length; i++) {
+ for(int j=0; j<_tr.blocks.length; j++) {
+ if (blocks[i] == blocks[j]) {
+ return true;
+ }
+ }
+ }
+
+ return false;
+ }
+
public boolean hasBlockIndex(int _index) {
if (blocksInt == null) {
return false;
--
GitLab