From 1e2977819f3b606a3349ae2c6df61d736a15c722 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Tue, 8 Mar 2022 10:57:08 +0100
Subject: [PATCH] Adding help on invariant, and reworking the help on
reachability graph, see ticket 258
---
modeling/AVATAR/CoffeeMachine_Avatar.xml | 4 +-
src/main/java/ui/TGUIAction.java | 5 ++-
src/main/resources/help/helpTable.txt | 1 +
src/main/resources/help/invariants.html | 45 +++++++++++++++++++
src/main/resources/help/invariants.md | 38 ++++++++++++++++
.../resources/help/reachabilitygraph.html | 14 ++++--
src/main/resources/help/reachabilitygraph.md | 4 ++
7 files changed, 103 insertions(+), 8 deletions(-)
create mode 100644 src/main/resources/help/invariants.html
create mode 100644 src/main/resources/help/invariants.md
diff --git a/modeling/AVATAR/CoffeeMachine_Avatar.xml b/modeling/AVATAR/CoffeeMachine_Avatar.xml
index c6af5a9745..06a2045474 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 a6f98b64e2..36754eaa4f 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 9e8e87dd81..740b9b7580 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 0000000000..114c3e2ed2
--- /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 0000000000..ba863565c5
--- /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 6308f762b0..4950ed9448 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 7cfd7b891a..5b5918a497 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
--
GitLab