From 6192fcdc6dc6ba8cd9da5db4ab6386a37addb54f Mon Sep 17 00:00:00 2001 From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr> Date: Mon, 17 Aug 2020 18:44:25 +0200 Subject: [PATCH] Update on help, including avatar pragmas --- modeling/AVATAR/CoffeeMachine_Avatar.xml | 183 +----------------- src/main/java/ui/TGHelpButton.java | 3 +- .../ui/avatarbd/AvatarBDSafetyPragma.java | 3 +- .../AvatarMethodologyDiagramName.java | 6 +- .../ui/window/JDialogAvatarModelChecker.java | 2 + .../java/ui/window/JDialogSafetyPragma.java | 35 +++- .../ui/window/JDialogTGComponentHelp.java | 2 +- src/main/resources/help/README | 6 +- src/main/resources/help/avatar.html | 6 +- src/main/resources/help/avatar.md | 6 +- src/main/resources/help/avatarbd.html | 36 ++++ src/main/resources/help/avatarbd.md | 25 +++ .../resources/help/avatarsafetypragmas.md | 17 ++ .../resources/help/avatarsoftwaredesign.html | 22 +++ .../resources/help/avatarsoftwaredesign.md | 4 + src/main/resources/help/helpTable.txt | 3 + 16 files changed, 162 insertions(+), 197 deletions(-) create mode 100644 src/main/resources/help/avatarbd.html create mode 100644 src/main/resources/help/avatarbd.md create mode 100644 src/main/resources/help/avatarsafetypragmas.md create mode 100644 src/main/resources/help/avatarsoftwaredesign.html create mode 100644 src/main/resources/help/avatarsoftwaredesign.md diff --git a/modeling/AVATAR/CoffeeMachine_Avatar.xml b/modeling/AVATAR/CoffeeMachine_Avatar.xml index 62cdf9c227..79ae804124 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="2" 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="0"> <Modeling type="Avatar Requirement" nameTab="AVATAR Requirements" > <AvatarRDPanel name="AVATAR RD" minX="10" maxX="1900" minY="10" maxY="1400" zoom="1.0" > @@ -1327,7 +1327,7 @@ </extraparam> </CONNECTOR> <COMPONENT type="303" id="716" > -<cdparam x="54" y="427" /> +<cdparam x="54" y="426" /> <sizeparam width="646" height="214" minWidth="80" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> <cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" /> @@ -4254,183 +4254,4 @@ CoffeeMachine.CoffeeDelivered --> CoffeeMachine.nbOfCoins<2 -<Modeling type="Avatar Methodology" nameTab="AVATAR_Methodology" > -<AvatarMethodologyDiagramPanel name="AVATAR_Methodology" minX="10" maxX="2500" minY="10" maxY="1500" zoom="1.0" > -<COMPONENT type="5605" id="2407" > -<cdparam x="200" y="400" /> -<sizeparam width="180" height="70" minWidth="10" minHeight="30" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="TGComponent" value="Properties" /> -<TGConnectingPoint num="0" id="2403" /> -<TGConnectingPoint num="1" id="2404" /> -<TGConnectingPoint num="2" id="2405" /> -<TGConnectingPoint num="3" id="2406" /> -</COMPONENT> - -<COMPONENT type="5606" id="2412" > -<cdparam x="550" y="500" /> -<sizeparam width="300" height="70" minWidth="10" minHeight="30" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="TGComponent" value="Prototyping" /> -<TGConnectingPoint num="0" id="2408" /> -<TGConnectingPoint num="1" id="2409" /> -<TGConnectingPoint num="2" id="2410" /> -<TGConnectingPoint num="3" id="2411" /> -</COMPONENT> - -<COMPONENT type="5604" id="2419" > -<cdparam x="450" y="400" /> -<sizeparam width="300" height="70" minWidth="10" minHeight="30" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="TGComponent" value="Design" /> -<TGConnectingPoint num="0" id="2414" /> -<TGConnectingPoint num="1" id="2415" /> -<TGConnectingPoint num="2" id="2416" /> -<TGConnectingPoint num="3" id="2417" /> -<TGConnectingPoint num="4" id="2418" /> -</COMPONENT> -<SUBCOMPONENT type="5607" id="2413" > -<father id="2419" num="0" /> -<cdparam x="455" y="440" /> -<sizeparam width="10" height="10" minWidth="10" minHeight="5" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="455" maxX="455" minY="440" maxY="440" /> -<infoparam name="value " value="AVATAR Design" /> -</SUBCOMPONENT> - -<COMPONENT type="5603" id="2425" > -<cdparam x="350" y="300" /> -<sizeparam width="200" height="70" minWidth="10" minHeight="30" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="TGComponent" value="Analysis" /> -<TGConnectingPoint num="0" id="2420" /> -<TGConnectingPoint num="1" id="2421" /> -<TGConnectingPoint num="2" id="2422" /> -<TGConnectingPoint num="3" id="2423" /> -<TGConnectingPoint num="4" id="2424" /> -</COMPONENT> - -<COMPONENT type="5602" id="2432" > -<cdparam x="250" y="200" /> -<sizeparam width="200" height="70" minWidth="10" minHeight="30" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="TGComponent" value="Requirements" /> -<TGConnectingPoint num="0" id="2426" /> -<TGConnectingPoint num="1" id="2427" /> -<TGConnectingPoint num="2" id="2428" /> -<TGConnectingPoint num="3" id="2429" /> -<TGConnectingPoint num="4" id="2430" /> -<TGConnectingPoint num="5" id="2431" /> -</COMPONENT> - -<COMPONENT type="5601" id="2437" > -<cdparam x="150" y="100" /> -<sizeparam width="200" height="70" minWidth="10" minHeight="30" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="TGComponent" value="Assumptions" /> -<TGConnectingPoint num="0" id="2433" /> -<TGConnectingPoint num="1" id="2434" /> -<TGConnectingPoint num="2" id="2435" /> -<TGConnectingPoint num="3" id="2436" /> -</COMPONENT> - -<CONNECTOR type="5608" id="2439" > -<cdparam x="270" y="270" /> -<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<infoparam name="connector" value="<<deriveReqt>>" /> -<TGConnectingPoint num="0" id="2438" /> -<P1 x="270" y="270" id="2428" /> -<P2 x="236" y="400" id="2403" /> -<AutomaticDrawing data="true" /> -</CONNECTOR> -<CONNECTOR type="5608" id="2443" > -<cdparam x="510" y="470" /> -<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<infoparam name="connector" value="<<deriveReqt>>" /> -<TGConnectingPoint num="0" id="2441" /> -<TGConnectingPoint num="1" id="2442" /> -<P1 x="510" y="470" id="2415" /> -<P2 x="550" y="535" id="2408" /> -<Point x="510" y="535" /> -<AutomaticDrawing data="true" /> -</CONNECTOR><SUBCOMPONENT type="-1" id="2440" > -<father id="2443" num="0" /> -<cdparam x="510" y="535" /> -<sizeparam width="8" height="8" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="point " value="null" /> -</SUBCOMPONENT> - -<CONNECTOR type="5608" id="2447" > -<cdparam x="410" y="370" /> -<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<infoparam name="connector" value="<<deriveReqt>>" /> -<TGConnectingPoint num="0" id="2445" /> -<TGConnectingPoint num="1" id="2446" /> -<P1 x="410" y="370" id="2421" /> -<P2 x="450" y="435" id="2414" /> -<Point x="410" y="435" /> -<AutomaticDrawing data="true" /> -</CONNECTOR><SUBCOMPONENT type="-1" id="2444" > -<father id="2447" num="0" /> -<cdparam x="410" y="435" /> -<sizeparam width="8" height="8" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="point " value="null" /> -</SUBCOMPONENT> - -<CONNECTOR type="5608" id="2451" > -<cdparam x="310" y="270" /> -<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<infoparam name="connector" value="<<deriveReqt>>" /> -<TGConnectingPoint num="0" id="2449" /> -<TGConnectingPoint num="1" id="2450" /> -<P1 x="310" y="270" id="2427" /> -<P2 x="350" y="335" id="2420" /> -<Point x="310" y="335" /> -<AutomaticDrawing data="true" /> -</CONNECTOR><SUBCOMPONENT type="-1" id="2448" > -<father id="2451" num="0" /> -<cdparam x="310" y="335" /> -<sizeparam width="8" height="8" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="point " value="null" /> -</SUBCOMPONENT> - -<CONNECTOR type="5608" id="2455" > -<cdparam x="210" y="170" /> -<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<infoparam name="connector" value="<<deriveReqt>>" /> -<TGConnectingPoint num="0" id="2453" /> -<TGConnectingPoint num="1" id="2454" /> -<P1 x="210" y="170" id="2433" /> -<P2 x="250" y="235" id="2426" /> -<Point x="210" y="235" /> -<AutomaticDrawing data="true" /> -</CONNECTOR><SUBCOMPONENT type="-1" id="2452" > -<father id="2455" num="0" /> -<cdparam x="210" y="235" /> -<sizeparam width="8" height="8" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> -<hidden value="false" /> -<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> -<infoparam name="point " value="null" /> -</SUBCOMPONENT> - - -</AvatarMethodologyDiagramPanel> - -</Modeling> - - - - </TURTLEGMODELING> \ No newline at end of file diff --git a/src/main/java/ui/TGHelpButton.java b/src/main/java/ui/TGHelpButton.java index 831bb0e8b0..a68450c253 100644 --- a/src/main/java/ui/TGHelpButton.java +++ b/src/main/java/ui/TGHelpButton.java @@ -120,8 +120,9 @@ public class TGHelpButton extends JButton { helpDialog.setLocationHelpWindow(but); } else { if(!helpDialog.isVisible()) { - helpDialog = new JDialogTGComponentHelp(mgui, he); + //helpDialog = new JDialogTGComponentHelp(mgui, he); helpDialog.setLocationHelpWindow(but); + helpDialog.setVisible(true); } else{ helpDialog.setVisible(false); } diff --git a/src/main/java/ui/avatarbd/AvatarBDSafetyPragma.java b/src/main/java/ui/avatarbd/AvatarBDSafetyPragma.java index 658c4f978d..c9fe007494 100644 --- a/src/main/java/ui/avatarbd/AvatarBDSafetyPragma.java +++ b/src/main/java/ui/avatarbd/AvatarBDSafetyPragma.java @@ -274,7 +274,8 @@ public class AvatarBDSafetyPragma extends TGCScalableWithoutInternalComponent { AvatarBDPanel abdp = (AvatarBDPanel) tdp; Map<String, List<String>> blockAttributeMap = abdp.getBlockStrings(true, true, true); - JDialogSafetyPragma jdn = new JDialogSafetyPragma(frame, "Setting the safety pragmas", value, blockAttributeMap); + JDialogSafetyPragma jdn = new JDialogSafetyPragma(frame, getTDiagramPanel().getMainGUI(), "Setting the safety pragmas", value, + blockAttributeMap); //jdn.setLocation(200, 150); jdn.setSize(500, 500); GraphicLib.centerOnParent(jdn); diff --git a/src/main/java/ui/avatarmethodology/AvatarMethodologyDiagramName.java b/src/main/java/ui/avatarmethodology/AvatarMethodologyDiagramName.java index 96811a62a3..d27411d48e 100755 --- a/src/main/java/ui/avatarmethodology/AvatarMethodologyDiagramName.java +++ b/src/main/java/ui/avatarmethodology/AvatarMethodologyDiagramName.java @@ -435,8 +435,7 @@ public class AvatarMethodologyDiagramName extends TGCScalableWithoutInternalComp } } - if (indexOnMe > -1) - { + if (indexOnMe > -1) { AvatarMethodologyDiagramReference ref = ((AvatarMethodologyDiagramReference)(getFather())); ref.makeCall(value, indexOnMe); } @@ -466,8 +465,7 @@ public class AvatarMethodologyDiagramName extends TGCScalableWithoutInternalComp } @Override - public void rescale(double scaleFactor) - { + public void rescale(double scaleFactor) { if ((valMinX != null) && (valMinX.length > 0)) { for (int i = 0; i < valMinX.length; i++) diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java index 7439a8c36d..b216e4d965 100644 --- a/src/main/java/ui/window/JDialogAvatarModelChecker.java +++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java @@ -233,6 +233,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act setButtons(); } + @SuppressWarnings("unchecked") protected void initComponents() { Container c = getContentPane(); @@ -288,6 +289,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act c01.gridwidth = GridBagConstraints.REMAINDER; //end row c01.anchor = GridBagConstraints.WEST; c01.fill = GridBagConstraints.HORIZONTAL; + wordRepresentationBox = new JComboBox(WORD_BITS); wordRepresentationBox.setSelectedIndex(wordRepresentationSelected); wordRepresentationBox.addActionListener(this); diff --git a/src/main/java/ui/window/JDialogSafetyPragma.java b/src/main/java/ui/window/JDialogSafetyPragma.java index 9aa14c8d9e..878fa0d469 100644 --- a/src/main/java/ui/window/JDialogSafetyPragma.java +++ b/src/main/java/ui/window/JDialogSafetyPragma.java @@ -38,6 +38,10 @@ package ui.window; +import help.HelpEntry; +import help.HelpManager; +import myutil.TraceManager; +import ui.MainGUI; import ui.util.IconManager; import javax.swing.*; @@ -79,11 +83,16 @@ public class JDialogSafetyPragma extends JDialogBase implements ActionListener { protected JPopupMenu helpPopup; private Map<String, List<String>> blockAttributeMap; + private JDialogTGComponentHelp helpDialog; + + protected MainGUI mgui; + /* * Creates new form */ - public JDialogSafetyPragma(Frame f, String title, String _text, Map<String, List<String>> blockAttributeMap) { + public JDialogSafetyPragma(Frame f, MainGUI _mgui, String title, String _text, Map<String, List<String>> blockAttributeMap) { super(f, title, true); + mgui = _mgui; text = _text; this.blockAttributeMap = blockAttributeMap; @@ -404,12 +413,34 @@ public class JDialogSafetyPragma extends JDialogBase implements ActionListener { } public void help() { + if (mgui == null) { + TraceManager.addDev("Null mgui"); + } + HelpManager hm = mgui.getHelpManager(); + HelpEntry he = hm.getHelpEntryWithHTMLFile("avatarsafetypragmas.html"); + if(helpDialog == null) { + helpDialog = new JDialogTGComponentHelp(mgui, he); + helpDialog.setLocationHelpWindow(help); + helpDialog.setSize(500, 500); + } else { + if(!helpDialog.isVisible()) { + //helpDialog = new JDialogTGComponentHelp(mgui, he); + helpDialog.setLocationHelpWindow(help); + helpDialog.setVisible(true); + } else{ + helpDialog.setVisible(false); + } + } + } + + + /*public void help() { if (!helpPopup.isVisible()) { helpPopup.show(help, 20, 20); } else { helpPopup.setVisible(false); } - } + }*/ public String getText() { return text; diff --git a/src/main/java/ui/window/JDialogTGComponentHelp.java b/src/main/java/ui/window/JDialogTGComponentHelp.java index b61f8850e2..fea0ee82c4 100644 --- a/src/main/java/ui/window/JDialogTGComponentHelp.java +++ b/src/main/java/ui/window/JDialogTGComponentHelp.java @@ -53,7 +53,7 @@ public class JDialogTGComponentHelp extends JDialog implements ActionListener { framePanel.add(helpPanel, BorderLayout.CENTER); - helpBut = new JButton("Help", IconManager.imgic32); + helpBut = new JButton("Open general help window", IconManager.imgic32); helpManager = new HelpManager(); if(helpManager.loadEntries()) { diff --git a/src/main/resources/help/README b/src/main/resources/help/README index 0594b29cc9..0913a1332d 100644 --- a/src/main/resources/help/README +++ b/src/main/resources/help/README @@ -1,7 +1,11 @@ How to specify a new entry? -1) name of html file +1) name of html file in helpTable.txt 2) master keyword 3) other keywords If keywords have multiple words, all words must be separated with "_" + +Then, add a new file in markdown format. DO NOT PUT A HTML file: the HTML file is automatically generated by TTool's Makefile: +- run make internalhelp +- then add the generated html to the git \ No newline at end of file diff --git a/src/main/resources/help/avatar.html b/src/main/resources/help/avatar.html index d1fcc9e7bf..f0c1821189 100644 --- a/src/main/resources/help/avatar.html +++ b/src/main/resources/help/avatar.html @@ -21,12 +21,12 @@ <h2 id="diagrams">Diagrams</h2> <p>The AVATAR profile reuses eight of the SysML diagrams (Package diagrams are not supported). AVATAR supports the following methodological phases:</p> <ul> -<li><p><em>Requirement capture</em>. Requirements and properties are structured using AVATAR Requirement Diagrams. At this step, properties are just defined with a specific label.</p></li> +<li><p><a href="file://requirements.html">Requirement capture</a>. Requirements and properties are structured using AVATAR Requirement Diagrams. At this step, properties are just defined with a specific label.</p></li> <li><p><strong>Assumption modeling</strong>. Assumptions of system may be captured with an assumption modeling diagram, based on a SysML requirement diagram.</p></li> <li><p><strong>System analysis</strong>. A system may be analyzed using Use Case Diagrams, Activity Diagrams and Sequence Diagrams.</p></li> -<li><p><strong>Software design</strong>. Software is designed in terms of communicating SysML blocks described in an AVATAR Block Diagram, and in terms of behaviors described with AVATAR State Machines.</p></li> +<li><p><a href="file://avatarsoftwaredesign.html">Software design</a>. Software is designed in terms of communicating SysML blocks described in an AVATAR Block Diagram, and in terms of behaviors described with AVATAR State Machines.</p></li> <li><p><strong>Property modeling</strong>. The formal semantics of properties is defined within TEPE Parametric Diagrams (PDs). Since TEPE PDs involve elements defined in system design (e.g, a given integer attribute of a block), TEPE PDs may be defined only after a first system design has been performed.</p></li> -<li><p>**Software deploiement* is performed with UML deploiement diagrams</p></li> +<li><p><strong>Software deploiement</strong> is performed with UML deploiement diagrams</p></li> </ul> <h2 id="verifications">Verifications</h2> <ul> diff --git a/src/main/resources/help/avatar.md b/src/main/resources/help/avatar.md index b8b3a0139e..c02cb04ca4 100644 --- a/src/main/resources/help/avatar.md +++ b/src/main/resources/help/avatar.md @@ -6,17 +6,17 @@ AVATAR stands for Automated Verification of reAl Time softwARe. AVATAR targets t The AVATAR profile reuses eight of the SysML diagrams (Package diagrams are not supported). AVATAR supports the following methodological phases: -- *Requirement capture*. Requirements and properties are structured using AVATAR Requirement Diagrams. At this step, properties are just defined with a specific label. +- [Requirement capture](file://requirements.md). Requirements and properties are structured using AVATAR Requirement Diagrams. At this step, properties are just defined with a specific label. - **Assumption modeling**. Assumptions of system may be captured with an assumption modeling diagram, based on a SysML requirement diagram. - **System analysis**. A system may be analyzed using Use Case Diagrams, Activity Diagrams and Sequence Diagrams. -- **Software design**. Software is designed in terms of communicating SysML blocks described in an AVATAR Block Diagram, and in terms of behaviors described with AVATAR State Machines. +- [Software design](file://avatarsoftwaredesign.md). Software is designed in terms of communicating SysML blocks described in an AVATAR Block Diagram, and in terms of behaviors described with AVATAR State Machines. - **Property modeling**. The formal semantics of properties is defined within TEPE Parametric Diagrams (PDs). Since TEPE PDs involve elements defined in system design (e.g, a given integer attribute of a block), TEPE PDs may be defined only after a first system design has been performed. -- **Software deploiement* is performed with UML deploiement diagrams +- **Software deploiement** is performed with UML deploiement diagrams ## Verifications - Formal verification can be performed from software design. Formal verification relies on internal tools (e.g. internal model-checker, reachability graph generator, graph minimization, test sequences generation) or UPPAAL. diff --git a/src/main/resources/help/avatarbd.html b/src/main/resources/help/avatarbd.html new file mode 100644 index 0000000000..6a08815485 --- /dev/null +++ b/src/main/resources/help/avatarbd.html @@ -0,0 +1,36 @@ +<!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%;} + </style> + <!--[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="avatar-block-diagram">AVATAR block diagram</h1> +<p>An AVATAR block diagram can be sued to describe the dtructure of a software in an abstract way.</p> +<p>The following modeling elements can be used for this purpose:</p> +<ul> +<li><p><strong>Blocks</strong>. A block corresponds to a software component. A block defines its own private attributes, methods and signals.</p></li> +<li><p><strong>Crypto blocks</strong>. Crypto blocks are blocks containing cryptographic methods</p></li> +<li><p><strong>Data type blocks</strong>. They can be used to define custom data types built upon baisc data types (integers, booleans).</p></li> +<li><p><strong>Library functions</strong> are meant to factorize the bahavior of blocks</p></li> +<li><p><strong>Crypto Library functions</strong> are library functions containing a set of cryptographic methods.</p></li> +</ul> +<p>Additionally, properties to be verified by this design are captured using pragmas:</p> +<ul> +<li><p><a href="file://avatarsafetypragmas.html">Safety pragmas</a></p></li> +<li><p>Security pragmas</p></li> +<li><p>Performance pragmas</p></li> +</ul> +</body> +</html> diff --git a/src/main/resources/help/avatarbd.md b/src/main/resources/help/avatarbd.md new file mode 100644 index 0000000000..648bc2bf80 --- /dev/null +++ b/src/main/resources/help/avatarbd.md @@ -0,0 +1,25 @@ +# AVATAR block diagram + +An AVATAR block diagram can be sued to describe the dtructure of a software in an abstract way. + +The following modeling elements can be used for this purpose: + +- **Blocks**. A block corresponds to a software component. A block defines its own private attributes, methods and signals. + +- **Crypto blocks**. Crypto blocks are blocks containing cryptographic methods + +- **Data type blocks**. They can be used to define custom data types built upon baisc data types (integers, booleans). + +- **Library functions** are meant to factorize the bahavior of blocks + +- **Crypto Library functions** are library functions containing a set of cryptographic methods. + + + +Additionally, properties to be verified by this design are captured using pragmas: + +- [Safety pragmas](file://avatarsafetypragmas.md) + +- Security pragmas + +- Performance pragmas \ No newline at end of file diff --git a/src/main/resources/help/avatarsafetypragmas.md b/src/main/resources/help/avatarsafetypragmas.md new file mode 100644 index 0000000000..c7d7288808 --- /dev/null +++ b/src/main/resources/help/avatarsafetypragmas.md @@ -0,0 +1,17 @@ +# AVATAR Safety pragmas + +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 + +## "E" properties + +## "Leads to" properties + +## True / False + + diff --git a/src/main/resources/help/avatarsoftwaredesign.html b/src/main/resources/help/avatarsoftwaredesign.html new file mode 100644 index 0000000000..0d75913f56 --- /dev/null +++ b/src/main/resources/help/avatarsoftwaredesign.html @@ -0,0 +1,22 @@ +<!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%;} + </style> + <!--[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="avatar-software-design">AVATAR Software design</h1> +<p>A software design is built upon an <a href="file://avatarbd">AVATAR block diagram</a> and a set of state machine diagrams.</p> +</body> +</html> diff --git a/src/main/resources/help/avatarsoftwaredesign.md b/src/main/resources/help/avatarsoftwaredesign.md new file mode 100644 index 0000000000..27bb370778 --- /dev/null +++ b/src/main/resources/help/avatarsoftwaredesign.md @@ -0,0 +1,4 @@ +# AVATAR Software design + +A software design is built upon an [AVATAR block diagram](file://avatarbd) and a set of state machine diagrams. + diff --git a/src/main/resources/help/helpTable.txt b/src/main/resources/help/helpTable.txt index fc5b294df9..bf1ee651c6 100644 --- a/src/main/resources/help/helpTable.txt +++ b/src/main/resources/help/helpTable.txt @@ -32,3 +32,6 @@ ---communicationmapping communicationmapping communication mapping - avatar avatar software embedded systems safety security -- requirements requirements satified satisfy derivereqt +-- avatarsoftwaredesign software_design avatar blocks software design +--- avatarbd avatar_block_diagram design software blocks +---- avatarsafetypragmas safety_properties safety properties pragmas ctl -- GitLab