diff --git a/modeling/AVATAR/CoffeeMachine_Avatar.xml b/modeling/AVATAR/CoffeeMachine_Avatar.xml
index 79ae804124930299f12c0e13dab23a3ffbf6a121..54f0dbbee3712a0d005ca60a69782508f8b8b1e1 100644
--- a/modeling/AVATAR/CoffeeMachine_Avatar.xml
+++ b/modeling/AVATAR/CoffeeMachine_Avatar.xml
@@ -1274,7 +1274,7 @@
<Modeling type="AVATAR Design" nameTab="AVATAR Design" tabs="Block Diagram$CoffeeButton$TeaButton$CoffeeMachine$Wallet" >
-<AVATARBlockDiagramPanel name="Block Diagram" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
+<AVATARBlockDiagramPanel name="Block Diagram" minX="6" maxX="896" minY="6" maxY="576" zoom="0.6400000000000001" >
<MainCode value="void __user_init() {"/>
<MainCode value="}"/>
<Optimized value="true" />
@@ -1283,12 +1283,12 @@
<Ignored value="" />
<CONNECTOR type="5002" id="695" >
-<cdparam x="321" y="567" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="205" y="362" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="640" maxHeight="1280" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from Block1 to Block0" value="" />
<TGConnectingPoint num="0" id="694" />
-<P1 x="560" y="351" id="773" />
-<P2 x="560" y="377" id="806" />
+<P1 x="357" y="224" id="773" />
+<P2 x="357" y="241" id="806" />
<AutomaticDrawing data="true" />
<extraparam>
<isd value="in pushCoffeeButton()" />
@@ -1297,12 +1297,12 @@
</extraparam>
</CONNECTOR>
<CONNECTOR type="5002" id="697" >
-<cdparam x="275" y="114" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="176" y="72" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="640" maxHeight="1280" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from Block0 to Block0" value="" />
<TGConnectingPoint num="0" id="696" />
-<P1 x="306" y="109" id="728" />
-<P2 x="445" y="108" id="802" />
+<P1 x="195" y="69" id="728" />
+<P2 x="284" y="69" id="802" />
<AutomaticDrawing data="true" />
<extraparam>
<iso value="in getCoin(int nbOfCoins)" />
@@ -1313,12 +1313,12 @@
</extraparam>
</CONNECTOR>
<CONNECTOR type="5002" id="699" >
-<cdparam x="623" y="565" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="398" y="361" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="640" maxHeight="1280" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from Block1 to Block0" value="" />
<TGConnectingPoint num="0" id="698" />
-<P1 x="790" y="350" id="748" />
-<P2 x="790" y="377" id="807" />
+<P1 x="505" y="223" id="748" />
+<P2 x="505" y="241" id="807" />
<AutomaticDrawing data="true" />
<extraparam>
<isd value="in pushTeaButton()" />
@@ -1327,12 +1327,12 @@
</extraparam>
</CONNECTOR>
<COMPONENT type="303" id="716" >
-<cdparam x="54" y="426" />
-<sizeparam width="646" height="214" minWidth="80" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="33" y="272" />
+<sizeparam width="441" height="148" minWidth="51" minHeight="6" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
+<cdrectangleparam minX="9" maxX="1399" minY="9" maxY="899" />
<infoparam name="UPPAAL Pragma" value="A[] CoffeeMachine.nbOfCoins<=2
-E<> CoffeeMachine.nbOfCoins>0
+T E<> CoffeeMachine.nbOfCoins>0
E<> CoffeeMachine.nbOfCoins>1
E[] CoffeeMachine.nbOfCoins<2
@@ -1340,11 +1340,11 @@ A[] Wallet.nbOfCoins<3
A[] Wallet.nbOfCoins>=0
E[] Wallet.nbOfCoins>=1
-CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered
+F CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered
CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered && CoffeeMachine.TeaDelivered
CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered || CoffeeMachine.TeaDelivered
CoffeeMachine.Beverage --> CoffeeMachine.WaitingForFirstCoin
-CoffeeMachine.WaitingForFirstCoin --> CoffeeMachine.EjectState
+F CoffeeMachine.WaitingForFirstCoin --> CoffeeMachine.EjectState
CoffeeMachine.WaitingForFirstCoin --> CoffeeMachine.EjectState || CoffeeMachine.WaitingForSecondCoin
CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2
@@ -1367,7 +1367,7 @@ CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2
<TGConnectingPoint num="15" id="715" />
<extraparam>
<Line value="A[] CoffeeMachine.nbOfCoins<=2" />
-<Line value="E<> CoffeeMachine.nbOfCoins>0" />
+<Line value="T E<> CoffeeMachine.nbOfCoins>0" />
<Line value="E<> CoffeeMachine.nbOfCoins>1" />
<Line value="E[] CoffeeMachine.nbOfCoins<2" />
<Line value="" />
@@ -1375,11 +1375,11 @@ CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2
<Line value="A[] Wallet.nbOfCoins>=0" />
<Line value="E[] Wallet.nbOfCoins>=1" />
<Line value="" />
-<Line value="CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered" />
+<Line value="F CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered" />
<Line value="CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered && CoffeeMachine.TeaDelivered" />
<Line value="CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered || CoffeeMachine.TeaDelivered" />
<Line value="CoffeeMachine.Beverage --> CoffeeMachine.WaitingForFirstCoin " />
-<Line value="CoffeeMachine.WaitingForFirstCoin --> CoffeeMachine.EjectState" />
+<Line value="F CoffeeMachine.WaitingForFirstCoin --> CoffeeMachine.EjectState" />
<Line value="CoffeeMachine.WaitingForFirstCoin --> CoffeeMachine.EjectState || CoffeeMachine.WaitingForSecondCoin" />
<Line value="" />
<Line value="CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2" />
@@ -1387,10 +1387,10 @@ CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2
</COMPONENT>
<COMPONENT type="5000" id="741" >
-<cdparam x="106" y="55" />
-<sizeparam width="200" height="218" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="67" y="35" />
+<sizeparam width="128" height="139" minWidth="3" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
+<cdrectangleparam minX="9" maxX="1399" minY="9" maxY="899" />
<infoparam name="Block0" value="Wallet" />
<TGConnectingPoint num="0" id="717" />
<TGConnectingPoint num="1" id="718" />
@@ -1430,10 +1430,10 @@ CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2
</COMPONENT>
<COMPONENT type="5000" id="816" >
-<cdparam x="445" y="19" />
-<sizeparam width="461" height="358" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="284" y="12" />
+<sizeparam width="295" height="229" minWidth="3" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
+<cdrectangleparam minX="9" maxX="1399" minY="9" maxY="899" />
<infoparam name="Block0" value="CoffeeMachine" />
<TGConnectingPoint num="0" id="792" />
<TGConnectingPoint num="1" id="793" />
@@ -1478,10 +1478,10 @@ CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2
</COMPONENT>
<SUBCOMPONENT type="5000" id="766" >
<father id="816" num="0" />
-<cdparam x="696" y="248" />
-<sizeparam width="189" height="102" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="445" y="158" />
+<sizeparam width="120" height="65" minWidth="3" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="272" minY="0" maxY="256" />
+<cdrectangleparam minX="0" maxX="175" minY="0" maxY="164" />
<infoparam name="Block1" value="TeaButton" />
<TGConnectingPoint num="0" id="742" />
<TGConnectingPoint num="1" id="743" />
@@ -1516,10 +1516,10 @@ CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="791" >
<father id="816" num="1" />
-<cdparam x="465" y="249" />
-<sizeparam width="190" height="102" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="297" y="159" />
+<sizeparam width="121" height="65" minWidth="3" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="271" minY="0" maxY="256" />
+<cdrectangleparam minX="0" maxX="174" minY="0" maxY="164" />
<infoparam name="Block1" value="CoffeeButton" />
<TGConnectingPoint num="0" id="767" />
<TGConnectingPoint num="1" id="768" />
diff --git a/src/main/java/ui/window/JDialogSafetyPragma.java b/src/main/java/ui/window/JDialogSafetyPragma.java
index 878fa0d469c8389a53676ea97ac6ddeed4fbdbb1..0b48cf9fb19090a19909f1b1f49ed70cc3545dee 100644
--- a/src/main/java/ui/window/JDialogSafetyPragma.java
+++ b/src/main/java/ui/window/JDialogSafetyPragma.java
@@ -83,7 +83,7 @@ public class JDialogSafetyPragma extends JDialogBase implements ActionListener {
protected JPopupMenu helpPopup;
private Map<String, List<String>> blockAttributeMap;
- private JDialogTGComponentHelp helpDialog;
+ //private JDialogTGComponentHelp helpDialog;
protected MainGUI mgui;
@@ -416,21 +416,26 @@ public class JDialogSafetyPragma extends JDialogBase implements ActionListener {
if (mgui == null) {
TraceManager.addDev("Null mgui");
}
+
HelpManager hm = mgui.getHelpManager();
HelpEntry he = hm.getHelpEntryWithHTMLFile("avatarsafetypragmas.html");
- if(helpDialog == null) {
+ mgui.openHelpFrame(he);
+
+ /*if(helpDialog == null) {
helpDialog = new JDialogTGComponentHelp(mgui, he);
helpDialog.setLocationHelpWindow(help);
- helpDialog.setSize(500, 500);
+ helpDialog.setSize(700, 600);
+ helpDialog.scrollToTop();
} else {
if(!helpDialog.isVisible()) {
//helpDialog = new JDialogTGComponentHelp(mgui, he);
helpDialog.setLocationHelpWindow(help);
+
helpDialog.setVisible(true);
} else{
helpDialog.setVisible(false);
}
- }
+ }*/
}
diff --git a/src/main/java/ui/window/JDialogTGComponentHelp.java b/src/main/java/ui/window/JDialogTGComponentHelp.java
index fea0ee82c45e1eeb6d620af3d100b7f23e80bccd..07459585679a937c5c5cfc2c686af493892f4d38 100644
--- a/src/main/java/ui/window/JDialogTGComponentHelp.java
+++ b/src/main/java/ui/window/JDialogTGComponentHelp.java
@@ -13,11 +13,12 @@ import java.awt.event.ActionListener;
public class JDialogTGComponentHelp extends JDialog implements ActionListener {
- MainGUI mainGUI;
- HelpEntry helpEntry;
- HelpManager helpManager;
- JButton helpBut;
- JEditorPane pane;
+ protected MainGUI mainGUI;
+ protected HelpEntry helpEntry;
+ protected HelpManager helpManager;
+ protected JButton helpBut;
+ protected JEditorPane pane;
+ protected JScrollPane jsp;
public JDialogTGComponentHelp(MainGUI _mgui, HelpEntry _he) {
@@ -113,4 +114,11 @@ public class JDialogTGComponentHelp extends JDialog implements ActionListener {
//TraceManager.addDev("help window location ==> (x,y) = " + "(" + dx+ "," + dy + ")" );
setLocation(dx, dy);
}
+
+ public void scrollToTop() {
+ if (jsp != null) {
+ jsp.getHorizontalScrollBar().setValue(0);
+ jsp.getVerticalScrollBar().setValue(0);
+ }
+ }
}
\ No newline at end of file
diff --git a/src/main/resources/help/CTLProperties.odg b/src/main/resources/help/CTLProperties.odg
new file mode 100644
index 0000000000000000000000000000000000000000..8e64b277816df0bb7537ff223eff175a008186db
Binary files /dev/null and b/src/main/resources/help/CTLProperties.odg differ
diff --git a/src/main/resources/help/avatarsafetypragmas.md b/src/main/resources/help/avatarsafetypragmas.md
index c7d7288808ac6648f2c6dc6da4472171c0d6f28c..92819d24398b70f0276b0c26613c7c1e109c36ea 100644
--- a/src/main/resources/help/avatarsafetypragmas.md
+++ b/src/main/resources/help/avatarsafetypragmas.md
@@ -3,15 +3,115 @@
A safety pragma expresses a property that is expected to be verified by the internal model checker or by UPPAAL.
A safety pragma is as follows, with p and q being properties:
+
- [T/F] A/E []/<> p
- [T/F] p --> q
-## "A" properties
+Example:
+T A<> Block1.x > 0
+means that the attribute "x" of block "Block1" is always strictly positive.
+
+
+## A[] p
+
+"A" means *on All paths* and "[]" means in *all states*. "A[] p" therefore means that "p" is expected to be satisfied in all states of all paths.
+
+<center>
+
+</center>
+
+
+## A<>p
+
+"A" means *on All paths* and "<>" means in *at least one state*. "A<> p" therefore means that "p" is expected to be satisfied in at least one state of all paths.
+
+<center>
+
+</center>
+
+
+
+## E[] properties
+"E" means *on one paths* and "[]" means in *all states*. "E<> p" therefore means that "p" is expected to be satisfied in at least all states of at least one path.
+
+<center>
+
+</center>
+
+
+
+## E<> properties
+
+<center>
+
+</center>
+
-## "E" properties
## "Leads to" properties
+"p --> q" means that whenever p is encoutred in a state s, all paths starting from state s must have a state in which q is satisfied.
+
+<center>
+
+</center>
+
## True / False
+A pragma may start with "T" or "F". "T" stands for True and "F" for False. T or F precise if the pragma is expected to be true or false during verification.
+- If a pragma starts with a "T" and is satisfied, then a green check is added on its left side.
+- if a pragma starts with a "T" and is not satisfied, then a red cross is added on its left side.
+- If a pragma starts with a "F" and is satisfied, then a red cross is added on its left side.
+- if a pragma starts with a "F" and is not satisfied, then a green check is added on its left side.
+
+Adding "T" or "F" before at the beginning of a pragma is **optional**. A pragma with no "T" or "F" is assumed to start with a "T".
+
+
+## "p" properties
+
+A pragma termines with a property. A property is a boolean expression. The following operators can be used between sub-boolean expressions:
+- "&&", "||"
+
+A boolean expression can:
+- State that a given state s of a block b has been reached: b.s
+- Use boolean or integer attributes of blocks, comparing them with operators such as : "==", "<", ">", ">=", "<="
+
+
+
+## Examples
+
+The following figures gives the pragmas that are given in the CoffeeMachine use case available on the model repository of TTool.
+
+- A[] CoffeeMachine.nbOfCoins<=2
+
+- T E<> CoffeeMachine.nbOfCoins>0
+
+- E<> CoffeeMachine.nbOfCoins>1
+
+- E[] CoffeeMachine.nbOfCoins<2
+
+- A[] Wallet.nbOfCoins<3
+
+- A[] Wallet.nbOfCoins>=0
+
+- E[] Wallet.nbOfCoins>=1
+
+- F CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered
+
+- CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered && CoffeeMachine.TeaDelivered
+
+- CoffeeMachine.Beverage --> CoffeeMachine.CoffeeDelivered || CoffeeMachine.TeaDelivered
+
+- CoffeeMachine.Beverage --> CoffeeMachine.WaitingForFirstCoin
+
+- F CoffeeMachine.WaitingForFirstCoin --> CoffeeMachine.EjectState
+
+- CoffeeMachine.WaitingForFirstCoin --> CoffeeMachine.EjectState || CoffeeMachine.WaitingForSecondCoin
+
+- CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2
+
+After verifying them with TTool's internal model checker, we obtain the following:
+<center>
+
+</center>
diff --git a/src/main/resources/help/ctlaall.png b/src/main/resources/help/ctlaall.png
new file mode 100644
index 0000000000000000000000000000000000000000..a05634fd72298d075fb74cb37ef8abf7d414f294
Binary files /dev/null and b/src/main/resources/help/ctlaall.png differ
diff --git a/src/main/resources/help/ctlaall_small.png b/src/main/resources/help/ctlaall_small.png
new file mode 100644
index 0000000000000000000000000000000000000000..9d72958f5ebd152d90b9516fb6575b2020d82f9b
Binary files /dev/null and b/src/main/resources/help/ctlaall_small.png differ
diff --git a/src/main/resources/help/ctlaone_small.png b/src/main/resources/help/ctlaone_small.png
new file mode 100644
index 0000000000000000000000000000000000000000..0098945fdebe49b85cb5ebbc72834193269d8862
Binary files /dev/null and b/src/main/resources/help/ctlaone_small.png differ
diff --git a/src/main/resources/help/ctleall.png b/src/main/resources/help/ctleall.png
new file mode 100644
index 0000000000000000000000000000000000000000..5d9fb4201a6f509e9aa933b3dd12d3656d0508c3
Binary files /dev/null and b/src/main/resources/help/ctleall.png differ
diff --git a/src/main/resources/help/ctleall_small.png b/src/main/resources/help/ctleall_small.png
new file mode 100644
index 0000000000000000000000000000000000000000..9d8f2352947332001ae738be77347d845b56430b
Binary files /dev/null and b/src/main/resources/help/ctleall_small.png differ
diff --git a/src/main/resources/help/ctleone_small.png b/src/main/resources/help/ctleone_small.png
new file mode 100644
index 0000000000000000000000000000000000000000..448ecbe5c10cb1b8ae724b76a7db0becb7e2acbb
Binary files /dev/null and b/src/main/resources/help/ctleone_small.png differ
diff --git a/src/main/resources/help/ctlleadsto_small.png b/src/main/resources/help/ctlleadsto_small.png
new file mode 100644
index 0000000000000000000000000000000000000000..0b3c1f27d8a10283c5a9579893528277ecef2947
Binary files /dev/null and b/src/main/resources/help/ctlleadsto_small.png differ
diff --git a/src/main/resources/help/pragmas_cm.png b/src/main/resources/help/pragmas_cm.png
new file mode 100644
index 0000000000000000000000000000000000000000..ccd139db5755ade1acdf89c9b075d991fabaa91d
Binary files /dev/null and b/src/main/resources/help/pragmas_cm.png differ