From e8480c09e093141c74045ced994b5b8c2821479e Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Thu, 15 Sep 2016 11:39:09 +0000
Subject: [PATCH] Update on mc code: bug on clock manipulation
---
modeling/testModelCheckerAvatar/testClocks.xml | 4 +---
src/avatartranslator/modelchecker/AvatarModelChecker.java | 8 ++++----
2 files changed, 5 insertions(+), 7 deletions(-)
diff --git a/modeling/testModelCheckerAvatar/testClocks.xml b/modeling/testModelCheckerAvatar/testClocks.xml
index f4c30bcc76..c0b63c4e18 100644
--- a/modeling/testModelCheckerAvatar/testClocks.xml
+++ b/modeling/testModelCheckerAvatar/testClocks.xml
@@ -7,7 +7,7 @@
<MainCode value="void __user_init() {"/>
<MainCode value="}"/>
<Optimized value="true" />
-<Validated value="" />
+<Validated value="B3;B2;B1;" />
<Ignored value="" />
<CONNECTOR type="5002" id="2" >
@@ -551,8 +551,6 @@
<afterMax value="30" />
<computeMin value="" />
<computeMax value="" />
-<filesToIncludeLine value="" />
-<codeToIncludeLine value="" />
</extraparam>
</SUBCOMPONENT>
diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index 50bd1d30ca..57b40909b6 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -652,17 +652,17 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Must compute the clockmin and clockmax values
String minDelay = _at.getMinDelay().trim();
if ((minDelay == null) || (minDelay.length() == 0)) {
- st.clockMin = 0 - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
+ st.clockMin = 0 - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
} else {
- st.clockMin = evaluateIntExpression(_at.getMinDelay(), _block, _sb) - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
+ st.clockMin = evaluateIntExpression(_at.getMinDelay(), _block, _sb) - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
}
String maxDelay = _at.getMaxDelay().trim();
if ((maxDelay == null) || (maxDelay.length() == 0)) {
- st.clockMax = 0 - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
+ st.clockMax = 0 - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
} else {
int resMax = evaluateIntExpression(_at.getMaxDelay(), _block, _sb);
_sb.maxClock = Math.max(_sb.maxClock, resMax);
- st.clockMax = resMax - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
+ st.clockMax = resMax - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
}
if (st.clockMin > st.clockMax) {
--
GitLab