From 0e90ecbf0fae4d8152fd201db6db557fc7772ec2 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Fri, 10 Jun 2016 08:32:53 +0000
Subject: [PATCH] Updating graph saving
---
...croWaveOven_SafetySecurity_fullMethodo.xml | 2 +-
.../modelchecker/AvatarModelChecker.java | 32 +++++++++++++------
2 files changed, 24 insertions(+), 10 deletions(-)
diff --git a/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml b/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml
index 3e543af08a..237888af94 100644
--- a/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml
+++ b/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml
@@ -5174,7 +5174,7 @@ or by a maintenance station
</CONNECTOR>
<COMPONENT type="302" id="2683" >
<cdparam x="382" y="26" />
-<sizeparam width="616" height="97" minWidth="80" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="668" height="97" minWidth="80" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
<infoparam name="Proverif Pragma" value="#InitialSystemKnowledge RemoteControl.PSK WirelessInterface.PSK
diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index 77a4157c86..8c4efb953d 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -239,7 +239,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
prepareTransitionsOfState(initialState);
blockValues = initialState.getBlockValues();
- //TraceManager.addDev("initialState=" + initialState.toString());
+ //TraceManager.addDev("initialState=" + initialState.toString() + " nbOfTransitions" + initialState.transitions.size());
initialState.computeHash(blockValues);
states.put(initialState.hashValue, initialState);
statesByID.put(initialState.id, initialState);
@@ -368,7 +368,15 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private void computeAllStatesFrom(SpecificationState _ss) {
+ if (_ss == null) {
+ mustStop();
+ return;
+ }
ArrayList<SpecificationTransition> transitions = _ss.transitions;
+ if (transitions == null) {
+ mustStop();
+ return;
+ }
//TraceManager.addDev("Possible transitions 1:" + transitions.size());
@@ -977,9 +985,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
sb.append("\nLinks:\n");
for(SpecificationState state: states.values()) {
- for(SpecificationLink link: state.nexts) {
- sb.append(link.toString() + "\n");
- }
+ if (state.nexts != null) {
+ for(SpecificationLink link: state.nexts) {
+ sb.append(link.toString() + "\n");
+ }
+ }
}
return sb.toString();
}
@@ -990,9 +1000,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
sb.append("des(0," + getNbOfLinks() + "," + getNbOfStates() + ")\n");
for(SpecificationState state: states.values()) {
- for(SpecificationLink link: state.nexts) {
+ if (state.nexts != null) {
+ for(SpecificationLink link: state.nexts) {
sb.append("(" + link.originState.id + ",\"" + link.action + "\"," + link.destinationState.id + ")\n");
- }
+ }
+ }
}
return new String(sb);
}
@@ -1002,10 +1014,12 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
sb.append("digraph TToolAvatarGraph {\n");
for(SpecificationState state: states.values()) {
- for(SpecificationLink link: state.nexts) {
+ if (state.nexts != null) {
+ for(SpecificationLink link: state.nexts) {
- sb.append(" " + link.originState.id + " -> " + link.destinationState.id + "[label=\"" + link.action + "\"];\n");
- }
+ sb.append(" " + link.originState.id + " -> " + link.destinationState.id + "[label=\"" + link.action + "\"];\n");
+ }
+ }
}
sb.append("}");
return new String(sb);
--
GitLab