diff --git a/simulators/c++2/src_simulator/definitions.h b/simulators/c++2/src_simulator/definitions.h
index 2cf89988ce176ca67ec4a4841ac8e1e8e46c2c61..5b79ca8c99acddb5d57e34dfe6fcdaf4c7afebcf 100644
--- a/simulators/c++2/src_simulator/definitions.h
+++ b/simulators/c++2/src_simulator/definitions.h
@@ -177,6 +177,8 @@ using std::max;
#define TAG_VARc "</var>"
#define TAG_STATUSo "<status>"
#define TAG_STATUSc "</status>"
+#define TAG_PENALTYo "<penalty>"
+#define TAG_PENALTYc "</penalty>"
#define TAG_REASONo "<brkreason>"
#define TAG_REASONc "</brkreason>"
#define TAG_GLOBALo "<global>"
diff --git a/simulators/c++2/src_simulator/sim/Simulator.cpp b/simulators/c++2/src_simulator/sim/Simulator.cpp
index 83a6d722c721888ca13de3c8aab82e37b888b008..1e9a2879fb6477a8f244ea46843983c9dcbf4ed7 100644
--- a/simulators/c++2/src_simulator/sim/Simulator.cpp
+++ b/simulators/c++2/src_simulator/sim/Simulator.cpp
@@ -1752,11 +1752,17 @@ void Simulator::decodeCommand(std::string iCmd, std::ostream &iXmlOutStream)
gettimeofday(&aBegin, NULL);
_busy = true;
// std::cout << "Not crashed. I: " << iCmd << std::endl;
+
anAckMsg << TAG_HEADER << std::endl
<< TAG_STARTo << std::endl
<< TAG_GLOBALo << std::endl
<< /*TAG_REPLYo << anIssuedCmd << TAG_REPLYc << std::endl<< */ TAG_MSGo << "Command received" << TAG_MSGc << TAG_ERRNOo << 0 << TAG_ERRNOc << std::endl
<< TAG_STATUSo << SIM_BUSY << TAG_STATUSc << std::endl
+ #ifdef PENALTIES_ENABLED
+ << TAG_PENALTYo << 1 << TAG_PENALTYc
+ #else
+ << TAG_PENALTYo << 0 << TAG_PENALTYc
+ #endif
<< TAG_GLOBALc << std::endl
<< TAG_STARTc << std::endl;
if (_replyToServer)
@@ -3494,7 +3500,13 @@ void Simulator::writeSimState(std::ostream &ioMessage)
}
else
{
- ioMessage << SIM_READY << TAG_STATUSc;
+ ioMessage << SIM_READY << TAG_STATUSc
+ #ifdef PENALTIES_ENABLED
+ << TAG_PENALTYo << 1 << TAG_PENALTYc
+ #else
+ << TAG_PENALTYo << 0 << TAG_PENALTYc
+ #endif
+ ;
if (_simComp->getStopReason() != "")
ioMessage << TAG_REASONo << _simComp->getStopReason() << TAG_REASONc;
}
diff --git a/src/main/java/ui/interactivesimulation/FormalVerificationToolBar.java b/src/main/java/ui/interactivesimulation/FormalVerificationToolBar.java
index 325e5f381a938a64af985304bf7b4eed787d2800..447447f205bf41cc6a9ff171a13b4eab96ac840d 100755
--- a/src/main/java/ui/interactivesimulation/FormalVerificationToolBar.java
+++ b/src/main/java/ui/interactivesimulation/FormalVerificationToolBar.java
@@ -63,7 +63,7 @@ public class FormalVerificationToolBar extends InteractiveSimulationBar {
protected void setActive(boolean b) {
jfis.actions[InteractiveSimulationActions.ACT_RESET_SIMU].setEnabled(b);
jfis.actions[InteractiveSimulationActions.ACT_STOP_SIMU].setEnabled(b);
- jfis.actions[InteractiveSimulationActions.ACT_RUN_EXPLORATION].setEnabled(b);
+ //jfis.actions[InteractiveSimulationActions.ACT_RUN_EXPLORATION].setEnabled(b);
jfis.actions[InteractiveSimulationActions.ACT_ANALYSIS_RG].setEnabled(b);
jfis.actions[InteractiveSimulationActions.ACT_VIEW_RG].setEnabled(b);
jfis.actions[InteractiveSimulationActions.ACT_REMOVE_ALL_TRANS].setEnabled(b);
diff --git a/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java b/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
index c04b87ed5c4ed2434a78f16c5980c78330b9a2dd..8553d8e1baf2e3d4fa756e361d92490667f1595e 100644
--- a/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
+++ b/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
@@ -43,6 +43,7 @@ import common.SpecConfigTTool;
import launcher.LauncherException;
import launcher.RshClient;
import myutil.*;
+import org.apache.batik.anim.timing.Trace;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
import org.w3c.dom.Node;
@@ -139,6 +140,8 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
protected StateCommandsToolBar stctb;
protected BenchmarkCommandsToolBar bctb;
protected FormalVerificationToolBar fvtb;
+ private boolean verificationActivated = false;
+ private JLabel warningPenalty;
// Commands
@@ -630,6 +633,8 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
fvtb = new FormalVerificationToolBar(this);
jp01.add(fvtb, BorderLayout.NORTH);
+ explorationEnabled();
+
jp02 = new JPanel();
gridbag01 = new GridBagLayout();
@@ -645,11 +650,11 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
// First empty line
c01.gridwidth = GridBagConstraints.REMAINDER; //end row
jp02.add(new JLabel(" "), c01);
- JLabel warning = new JLabel("Beware: Formal Verification ignores Penalties");
- Font newLabelFont=new Font(warning.getFont().getName(),Font.ITALIC,warning.getFont().getSize());
+ warningPenalty = new JLabel("Beware: Exploration requires deactivated penalties");
+ Font newLabelFont=new Font(warningPenalty.getFont().getName(),Font.ITALIC,warningPenalty.getFont().getSize());
//Set JLabel font using new created font
- warning.setFont(newLabelFont);
- jp02.add(warning, c01);
+ warningPenalty.setFont(newLabelFont);
+ jp02.add(warningPenalty, c01);
jp02.add(new JLabel(" "), c01);
// Line minimum command: labels
@@ -2116,6 +2121,15 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
makeStatus(node0.getTextContent());
}
+ nl = elt.getElementsByTagName("penalty");
+
+ if ((nl != null) && (nl.getLength() > 0)) {
+ node0 = nl.item(0);
+ //
+ //TraceManager.addDev("******* PENALTY INFO *******");
+ makePenaltyInformation(node0.getTextContent());
+ }
+
nl = elt.getElementsByTagName("brkreason");
if ((nl != null) && (nl.getLength() > 0)) {
node0 = nl.item(0);
@@ -2626,6 +2640,30 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
info.setText(s);
}
+ public void makePenaltyInformation(String s) {
+ //TraceManager.addDev("Penalties activated? " + s);
+ if (s.equals("1")) {
+ verificationActivated = false;
+ } else {
+ verificationActivated = true;
+ }
+ explorationEnabled();
+ }
+
+ public void explorationEnabled() {
+ fvtb.setEnabled(verificationActivated);
+ if (warningPenalty != null) {
+ if (verificationActivated) {
+ warningPenalty.setText("Exploration enabled because penalties are deactivated");
+ } else {
+ warningPenalty.setText("Exploration disabled because penalties are activated");
+ }
+ }
+ if (!verificationActivated) {
+ actions[InteractiveSimulationActions.ACT_RUN_EXPLORATION].setEnabled(verificationActivated);
+ }
+ }
+
public void makeStatus(String s) {
//
@@ -2704,7 +2742,7 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
actions[InteractiveSimulationActions.ACT_RUN_X_COMMANDS].setEnabled(b);
actions[InteractiveSimulationActions.ACT_RESET_SIMU].setEnabled(b);
actions[InteractiveSimulationActions.ACT_STOP_SIMU].setEnabled(b);
- actions[InteractiveSimulationActions.ACT_RUN_EXPLORATION].setEnabled(b);
+ actions[InteractiveSimulationActions.ACT_RUN_EXPLORATION].setEnabled(b&&verificationActivated);
actions[InteractiveSimulationActions.ACT_REMOVE_ALL_TRANS].setEnabled(b);
if (jpsv != null) {
diff --git a/src/main/java/ui/interactivesimulation/MainCommandsToolBar.java b/src/main/java/ui/interactivesimulation/MainCommandsToolBar.java
index 620d030123541aa08d0268de73fab6b4671dc2e2..205ec91a222fc26c1889e894bedf851639e69e1c 100755
--- a/src/main/java/ui/interactivesimulation/MainCommandsToolBar.java
+++ b/src/main/java/ui/interactivesimulation/MainCommandsToolBar.java
@@ -67,7 +67,7 @@ public class MainCommandsToolBar extends InteractiveSimulationBar {
jfis.actions[InteractiveSimulationActions.ACT_RUN_TO_TIME].setEnabled(b);
jfis.actions[InteractiveSimulationActions.ACT_RUN_X_TRANSACTIONS].setEnabled(b);
jfis.actions[InteractiveSimulationActions.ACT_RUN_X_COMMANDS].setEnabled(b);
- jfis.actions[InteractiveSimulationActions.ACT_RUN_EXPLORATION].setEnabled(b);
+ //jfis.actions[InteractiveSimulationActions.ACT_RUN_EXPLORATION].setEnabled(b);
jfis.actions[InteractiveSimulationActions.ACT_RUN_TO_NEXT_BUS_TRANSFER].setEnabled(b);
jfis.actions[InteractiveSimulationActions.ACT_RUN_UNTIL_CPU_EXECUTES].setEnabled(b);
jfis.actions[InteractiveSimulationActions.ACT_RUN_UNTIL_TASK_EXECUTES].setEnabled(b);