diff --git a/modeling/AVATAR/CoffeeMachine_Avatar.xml b/modeling/AVATAR/CoffeeMachine_Avatar.xml
index c6af5a9745ab2dad535919415a0c583fb5de3fd3..06a2045474deed51bf3562aa49ca43b8e8d33bbc 100644
--- a/modeling/AVATAR/CoffeeMachine_Avatar.xml
+++ b/modeling/AVATAR/CoffeeMachine_Avatar.xml
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8"?>
-<TURTLEGMODELING version="1.0beta" ANIMATE_INTERACTIVE_SIMULATION="false" ACTIVATE_PENALTIES="true" UPDATE_INFORMATION_DIPLO_SIM="false" ANIMATE_WITH_INFO_DIPLO_SIM="true" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="1" LAST_SELECTED_SUB_TAB="0">
+<TURTLEGMODELING version="1.0beta" ANIMATE_INTERACTIVE_SIMULATION="false" ACTIVATE_PENALTIES="true" UPDATE_INFORMATION_DIPLO_SIM="false" ANIMATE_WITH_INFO_DIPLO_SIM="true" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="1" LAST_SELECTED_SUB_TAB="1">
<Modeling type="Avatar Requirement" nameTab="AVATAR Requirements" >
<AvatarRDPanel name="AVATAR RD" minX="10" maxX="1900" minY="10" maxY="1400" zoom="1.0" >
@@ -1395,7 +1395,7 @@
<MainCode value="}"/>
<Optimized value="true" />
<considerTimingOperators value="true" />
-<Validated value="Wallet;CoffeeMachine;CoffeeButton;TeaButton;" />
+<Validated value="" />
<Ignored value="" />
<CONNECTOR type="5002" id="771" index="0" uid="f480e606-bbb6-4ab7-8f89-8abb37ff40bb" >
diff --git a/src/main/java/ui/TGUIAction.java b/src/main/java/ui/TGUIAction.java
index a6f98b64e26e7648bdb76dd773858ab3f6a708f0..36754eaa4f2890491461a3f5206f1bb9795d2355 100644
--- a/src/main/java/ui/TGUIAction.java
+++ b/src/main/java/ui/TGUIAction.java
@@ -939,8 +939,9 @@ public class TGUIAction extends AbstractAction {
actions[ACT_AVATAR_SIM] = new TAction("avatar-simu", "Interactive simulation", IconManager.imgic18, IconManager.imgic18, "Interactive simulation", "Interactive simulation of the AVATAR design under edition", '2');
actions[ACT_AVATAR_FV_UPPAAL] = new TAction("avatar-formal-verification-uppaal", "Safety formal verification with UPPAAL (Safety)", IconManager.imgic86, IconManager.imgic86, "Formal verification with UPPAAL (Safety)", "Formal verification with UPPAAL (Safety) of the AVATAR design under edition", '3');
actions[ACT_AVATAR_FV_PROVERIF] = new TAction("avatar-formal-verification-proverif", "Security verification (ProVerif)", IconManager.imgic88, IconManager.imgic88, "Security verification (ProVerif)", "Security formal verification (with ProVerif)", '4');
- actions[ACT_AVATAR_FV_STATICANALYSIS] = new TAction("avatar-formal-verification-staticanalysis", "Safety analysis (invariants)",
- IconManager.imgic96, IconManager.imgic96, "Safaty analysis (invariants)", "Safety analysis using the invariant technique", '5');
+ actions[ACT_AVATAR_FV_STATICANALYSIS] = new TAction("avatar-formal-verification-staticanalysis", "Mutual exclusion analysis",
+ IconManager.imgic96, IconManager.imgic96, "Mutual exclusion analysis with invariants", "Mutual exclusion analysis with invariants",
+ '5');
actions[ACT_AVATAR_EXECUTABLE_GENERATION] = new TAction("avatar-executable-generation", "Code generation" , IconManager.imgic94, IconManager.imgic94, "Code generation", "Generation of C-POSIX executable code from AVATAR design under edition", '6');
diff --git a/src/main/resources/help/helpTable.txt b/src/main/resources/help/helpTable.txt
index 9e8e87dd8114631893205add44b9d880f74c09c0..740b9b7580781edd05b1d80d6265de3ecbcb8f29 100644
--- a/src/main/resources/help/helpTable.txt
+++ b/src/main/resources/help/helpTable.txt
@@ -42,6 +42,7 @@
--- avatarbd avatar_block_diagram design software blocks
---- avatarsafetypragmas safety_properties safety properties pragmas ctl
--- reachabilitygraph reachability_graph reachability graph display show nodes edges node edge
+--- invariants invariant invariant petri net mutual exclusion safety verification
--- avatarsimulation avatar_simulation interactive statistics
---- avatarstatistics avatar_statistics simulation avatar interactive statistics
diff --git a/src/main/resources/help/invariants.html b/src/main/resources/help/invariants.html
new file mode 100644
index 0000000000000000000000000000000000000000..114c3e2ed2eeeafeca1445fcf409110073f41319
--- /dev/null
+++ b/src/main/resources/help/invariants.html
@@ -0,0 +1,45 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
+<head>
+ <meta charset="utf-8" />
+ <meta name="generator" content="pandoc" />
+ <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
+ <title>TTool help</title>
+ <style>
+ code{white-space: pre-wrap;}
+ span.smallcaps{font-variant: small-caps;}
+ span.underline{text-decoration: underline;}
+ div.column{display: inline-block; vertical-align: top; width: 50%;}
+ div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
+ ul.task-list{list-style: none;}
+ .display.math{display: block; text-align: center; margin: 0.5rem auto;}
+ </style>
+ <link rel="stylesheet" href="/Users/ludovicapvrille/TTool/src/main/resources/help/help.css" />
+ <!--[if lt IE 9]>
+ <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
+ <![endif]-->
+</head>
+<body>
+<h1 id="invariants">Invariants</h1>
+<h2 id="what-are-invariants">What are invariants?</h2>
+<p>P-invariants (or place invariants) of Petri Nets can be used to prove mutual exclusion properties.</p>
+<p>For more information, see: Apvrille, Ludovic and Saqui-Sannes, Pierre de Static analysis techniques to verify mutual exclusion situations within SysML models. ( In Press: 2013) In: SDL 2013 - 16th International System Design Languages Forum, 26-28 Jun 2013, Montreal, Canada</p>
+<p>You can also access to the paper as follows: https://oatao.univ-toulouse.fr/8846/1/Saqui-Sannes_8846.pdf</p>
+<h2 id="invariants-in-avatar-models">Invariants in Avatar models</h2>
+<p>In the scope of Avatar, P-invariants, or invariants for short, can be used to prove mutual exclusion between states of state machine diagrams. To compute invariants, TTool first translates an Avatar model into a Petri net. Then, it computes the incidence matrix of that Petri net. Finally, it relies on the Farkas algorithm to compute mutual exclusion between states.</p>
+<h2 id="how-to-proceed">how to proceed</h2>
+<ol type="1">
+<li>Select states of states machines for which you would like to study mutual exclusion. for this, do a right click on a state and select “Check for mutual exclusionâ€. This stage is optional since in stage 4. you can select to study the mutual exclusion between all states of your state machine diagrams.</li>
+<li>Check the syntax of the model. We now assume the syntax of the model produces no error.</li>
+<li>Click on the “Mutual exclusion analysis†icon. A window shall open.</li>
+<li>Select optins and click on start. Mutual exclusion (as well as other intermediate models) are given in the tabs of the dialog window.</li>
+</ol>
+<h2 id="backtracing-to-models">Backtracing to models</h2>
+<p>Once computed, mutual exclusions are displayed next to each state of the state machine.</p>
+<h2 id="limitations">Limitations</h2>
+<ul>
+<li>Combinatory explosion</li>
+<li>Timing operators (after clauses, timers) are ignored</li>
+</ul>
+</body>
+</html>
diff --git a/src/main/resources/help/invariants.md b/src/main/resources/help/invariants.md
new file mode 100644
index 0000000000000000000000000000000000000000..ba863565c579a2a2d5b05206823c3307ea330f49
--- /dev/null
+++ b/src/main/resources/help/invariants.md
@@ -0,0 +1,38 @@
+# Invariants
+
+## What are invariants?
+
+P-invariants (or place invariants) of Petri Nets can be used to prove mutual exclusion properties.
+
+For more information, see:
+Apvrille, Ludovic and Saqui-Sannes, Pierre de Static
+analysis techniques to verify mutual exclusion situations within SysML models. (
+In Press: 2013) In: SDL 2013 - 16th International System Design Languages
+Forum, 26-28 Jun 2013, Montreal, Canada
+
+You can also access to the paper as follows:
+https://oatao.univ-toulouse.fr/8846/1/Saqui-Sannes_8846.pdf
+
+
+## Invariants in Avatar models
+ In the scope of Avatar, P-invariants, or invariants for short, can be used to prove mutual exclusion between states of state machine diagrams. To compute invariants, TTool first translates an Avatar model into a Petri net. Then, it computes the incidence matrix of that Petri net. Finally, it relies on the Farkas algorithm to compute mutual exclusion between states.
+
+
+## how to proceed
+
+1. Select states of states machines for which you would like to study mutual exclusion. for this, do a right click on a state and select "Check for mutual exclusion". This stage is optional since in stage 4. you can select to study the mutual exclusion between all states of your state machine diagrams.
+2. Check the syntax of the model. We now assume the syntax of the model produces no error.
+3. Click on the "Mutual exclusion analysis" icon. A window shall open.
+4. Select optins and click on start. Mutual exclusion (as well as other intermediate models) are given in the tabs of the dialog window.
+
+
+## Backtracing to models
+Once computed, mutual exclusions are displayed next to each state of the state machine.
+
+
+## Limitations
+- Combinatory explosion
+- Timing operators (after clauses, timers) are ignored
+
+
+
diff --git a/src/main/resources/help/reachabilitygraph.html b/src/main/resources/help/reachabilitygraph.html
index 6308f762b07250d101970723d07c12b7def5cd47..4950ed9448e94dcbc52dbbe3bfa622e25a199448 100644
--- a/src/main/resources/help/reachabilitygraph.html
+++ b/src/main/resources/help/reachabilitygraph.html
@@ -6,17 +6,23 @@
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
<title>TTool help</title>
<style>
- code{white-space: pre-wrap;}
- span.smallcaps{font-variant: small-caps;}
- span.underline{text-decoration: underline;}
- div.column{display: inline-block; vertical-align: top; width: 50%;}
+ code{white-space: pre-wrap;}
+ span.smallcaps{font-variant: small-caps;}
+ span.underline{text-decoration: underline;}
+ div.column{display: inline-block; vertical-align: top; width: 50%;}
+ div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
+ ul.task-list{list-style: none;}
+ .display.math{display: block; text-align: center; margin: 0.5rem auto;}
</style>
+ <link rel="stylesheet" href="/Users/ludovicapvrille/TTool/src/main/resources/help/help.css" />
<!--[if lt IE 9]>
<script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
<![endif]-->
</head>
<body>
<h1 id="reachability-graphs">Reachability graphs</h1>
+<h2 id="what-is-a-reachability-graph">What is a reachability graph?</h2>
+<p>A reachability graph (RG) represents all possible execution paths and states of a system. Here, a reachability graph is produced from an Avatar design. To be generated, the graph generator considers all possibles transitions from states of states machine, independently from the probabilities attached to transitions between the states of state machines. Said differently, the graph generator considers all possible transitions between states of states machines. So, even transitions with low probability are in the RG.</p>
<h2 id="how-to-generate-a-reachability-graph">How to generate a reachability graph?</h2>
<p>Reachability Graphs can be created by using the internal model-checker of TTool. This video on formal verification details the steps to generate a RG: https://www.youtube.com/watch?v=8IYJ1UDUbvQ</p>
<h2 id="working-with-rgs">Working with RGs</h2>
diff --git a/src/main/resources/help/reachabilitygraph.md b/src/main/resources/help/reachabilitygraph.md
index 7cfd7b891ae6b878f0e2b7ab75f1d665798a18dd..5b5918a497c113dc2d2327f43a27df6deb9283cd 100644
--- a/src/main/resources/help/reachabilitygraph.md
+++ b/src/main/resources/help/reachabilitygraph.md
@@ -1,5 +1,9 @@
# Reachability graphs
+## What is a reachability graph?
+A reachability graph (RG) represents all possible execution paths and states of a system. Here, a reachability graph is produced from an Avatar design.
+To be generated, the graph generator considers all possibles transitions from states of states machine, independently from the probabilities attached to transitions between the states of state machines. Said differently, the graph generator considers all possible transitions between states of states machines. So, even transitions with low probability are in the RG.
+
## How to generate a reachability graph?
Reachability Graphs can be created by using the internal model-checker of TTool.
This video on formal verification details the steps to generate a RG: https://www.youtube.com/watch?v=8IYJ1UDUbvQ