From b203efbbf459636a06d81b5b60aa145fde516aa0 Mon Sep 17 00:00:00 2001 From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr> Date: Wed, 8 Nov 2023 08:42:46 +0100 Subject: [PATCH] Update on variable management in Avatar --- .../avatartranslator/modelchecker/AvatarModelChecker.java | 4 ++++ .../java/avatartranslator/toexecutable/AVATAR2CPOSIX.java | 4 ++++ .../java/avatartranslator/toproverif/AVATAR2ProVerif.java | 4 ++++ src/main/java/avatartranslator/tosysmlv2/AVATAR2SysMLV2.java | 3 +++ src/main/java/avatartranslator/totpn/AVATAR2TPN.java | 4 ++++ src/main/java/avatartranslator/touppaal/AVATAR2UPPAAL.java | 4 ++++ 6 files changed, 23 insertions(+) diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java index 7e95f090c8..a06dfd34c8 100644 --- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java +++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java @@ -41,6 +41,7 @@ package avatartranslator.modelchecker; import avatartranslator.*; import avatartranslator.intboolsolver.AvatarIBSExpressions; +import avatartranslator.intboolsolver.AvatarIBSolver; import myutil.BoolExpressionEvaluator; import myutil.Conversion; import myutil.IntExpressionEvaluator; @@ -926,6 +927,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { spec.setAttributeOptRatio(compressionFactor); spec.generateAllExpressionSolvers(); + // Reset parser + AvatarIBSolver.clearAttributes(); + prepareTransitions(); prepareBlocks(); diff --git a/src/main/java/avatartranslator/toexecutable/AVATAR2CPOSIX.java b/src/main/java/avatartranslator/toexecutable/AVATAR2CPOSIX.java index e0f1f8c279..fb256804e3 100755 --- a/src/main/java/avatartranslator/toexecutable/AVATAR2CPOSIX.java +++ b/src/main/java/avatartranslator/toexecutable/AVATAR2CPOSIX.java @@ -44,6 +44,7 @@ import java.util.List; import java.util.Vector; import avatartranslator.*; +import avatartranslator.intboolsolver.AvatarIBSolver; import common.SpecConfigTTool; import myutil.Conversion; import myutil.FileException; @@ -162,6 +163,9 @@ public class AVATAR2CPOSIX { avspec.removeLibraryFunctionCalls(); avspec.removeTimers(); + // Reset parser + AvatarIBSolver.clearAttributes(); + //TraceManager.addDev("AVATAR2CPOSIX avspec=" + avspec); diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java index 6dd9171ebe..0e6d5bba08 100755 --- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java +++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java @@ -39,6 +39,7 @@ package avatartranslator.toproverif; import avatartranslator.*; +import avatartranslator.intboolsolver.AvatarIBSolver; import common.ConfigurationTTool; import myutil.FileException; import myutil.FileUtils; @@ -450,6 +451,9 @@ public class AVATAR2ProVerif implements AvatarTranslator { this.avspec.removeTimers(); + // Reset parser + AvatarIBSolver.clearAttributes(); + this.dummyDataCounter = 0; List<AvatarAttribute> allKnowledge = this.makeStartingProcess(); diff --git a/src/main/java/avatartranslator/tosysmlv2/AVATAR2SysMLV2.java b/src/main/java/avatartranslator/tosysmlv2/AVATAR2SysMLV2.java index 22f948363f..1e5e6b0b99 100644 --- a/src/main/java/avatartranslator/tosysmlv2/AVATAR2SysMLV2.java +++ b/src/main/java/avatartranslator/tosysmlv2/AVATAR2SysMLV2.java @@ -47,6 +47,7 @@ import java.util.Scanner; import java.util.Vector; import avatartranslator.*; +import avatartranslator.intboolsolver.AvatarIBSolver; import common.SpecConfigTTool; import myutil.Conversion; import myutil.FileException; @@ -165,6 +166,8 @@ public class AVATAR2SysMLV2 { avspec.removeCompositeStates(); avspec.removeLibraryFunctionCalls(); avspec.removeTimers(); + // Reset parser + AvatarIBSolver.clearAttributes(); //TraceManager.addDev("AVATAR2CPOSIX avspec=" + avspec); diff --git a/src/main/java/avatartranslator/totpn/AVATAR2TPN.java b/src/main/java/avatartranslator/totpn/AVATAR2TPN.java index a7574f70e6..d3a26b67b8 100755 --- a/src/main/java/avatartranslator/totpn/AVATAR2TPN.java +++ b/src/main/java/avatartranslator/totpn/AVATAR2TPN.java @@ -42,6 +42,7 @@ package avatartranslator.totpn; import avatartranslator.*; +import avatartranslator.intboolsolver.AvatarIBSolver; import myutil.TraceManager; import tpndescription.Place; import tpndescription.TPN; @@ -104,6 +105,9 @@ public class AVATAR2TPN { avspec.removeLibraryFunctionCalls (); avspec.removeTimers(); + // Reset parser + AvatarIBSolver.clearAttributes(); + makeBlocks(); //TraceManager.addDev("-> tpn:" + tpn.toString()); diff --git a/src/main/java/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/main/java/avatartranslator/touppaal/AVATAR2UPPAAL.java index 55dab417ef..7a76a72de0 100755 --- a/src/main/java/avatartranslator/touppaal/AVATAR2UPPAAL.java +++ b/src/main/java/avatartranslator/touppaal/AVATAR2UPPAAL.java @@ -39,6 +39,7 @@ package avatartranslator.touppaal; import avatartranslator.*; +import avatartranslator.intboolsolver.AvatarIBSolver; import common.SpecConfigTTool; import myutil.Conversion; import myutil.FileException; @@ -164,6 +165,9 @@ public class AVATAR2UPPAAL { avspec.removeTimers(); //avspec.removeElseGuards(); + // Reset parser + AvatarIBSolver.clearAttributes(); + //avspec.removeFIFOs(2); avspec.makeRobustness(); -- GitLab