deploy: b3533fc

UPPAALModelChecker · Apr 16, 2024 · 3980df5 · 3980df5
1 parent 959cdfe
commit 3980df5
Show file tree

Hide file tree

Showing 85 changed files with 332 additions and 334 deletions.
diff --git a/404.html b/404.html
@@ -1,2 +1,2 @@
 <!doctype html><html lang=en class="js csstransforms3d"><head><meta charset=utf-8><meta name=description content><link rel=icon href=/images/favicon.png type=image/png><title>404 Page not found</title>
-<link href=/css/nucleus.css?1710941466 rel=stylesheet><link href=/css/fontawesome-all.min.css?1710941466 rel=stylesheet><link href=/css/hybrid.css?1710941466 rel=stylesheet><link href=/css/featherlight.min.css?1710941466 rel=stylesheet><link href=/css/perfect-scrollbar.min.css?1710941466 rel=stylesheet><link href=/css/theme.css?1710941466 rel=stylesheet><link href=/css/hugo-theme.css?1710941466 rel=stylesheet><style>:root #header+#content>#left>#rlblock_left{display:none!important}p,li,ul{text-align:center}ul{list-style-type:none}</style></head><body data-url=/><section id=body style=margin-left:0><div id=overlay></div><div id=chapter><div id=body-inner><h1>Error</h1><p></p><p>Woops. Looks like this page doesn't exist ¯\_(ツ)_/¯.</p><p></p><p><a href=/>Go to homepage</a></p><p><img src=/images/gopher-404.jpg style=width:50% alt="Page not found!"></p></div></div></section></body></html>
+<link href=/css/nucleus.css?1713244683 rel=stylesheet><link href=/css/fontawesome-all.min.css?1713244683 rel=stylesheet><link href=/css/hybrid.css?1713244683 rel=stylesheet><link href=/css/featherlight.min.css?1713244683 rel=stylesheet><link href=/css/perfect-scrollbar.min.css?1713244683 rel=stylesheet><link href=/css/theme.css?1713244683 rel=stylesheet><link href=/css/hugo-theme.css?1713244683 rel=stylesheet><style>:root #header+#content>#left>#rlblock_left{display:none!important}p,li,ul{text-align:center}ul{list-style-type:none}</style></head><body data-url=/><section id=body style=margin-left:0><div id=overlay></div><div id=chapter><div id=body-inner><h1>Error</h1><p></p><p>Woops. Looks like this page doesn't exist ¯\_(ツ)_/¯.</p><p></p><p><a href=/>Go to homepage</a></p><p><img src=/images/gopher-404.jpg style=width:50% alt="Page not found!"></p></div></div></section></body></html>
diff --git a/categories/index.html b/categories/index.html
diff --git a/extensions/cora/index.html b/extensions/cora/index.html
diff --git a/extensions/ecdar/index.html b/extensions/ecdar/index.html
diff --git a/extensions/index.html b/extensions/index.html
diff --git a/extensions/tiga/index.html b/extensions/tiga/index.html
diff --git a/extensions/tron/index.html b/extensions/tron/index.html
diff --git a/gui-reference/concrete-simulator/gantt-chart/index.html b/gui-reference/concrete-simulator/gantt-chart/index.html
diff --git a/gui-reference/concrete-simulator/index.html b/gui-reference/concrete-simulator/index.html
diff --git a/gui-reference/concrete-simulator/process/index.html b/gui-reference/concrete-simulator/process/index.html
diff --git a/gui-reference/concrete-simulator/sequence-chart/index.html b/gui-reference/concrete-simulator/sequence-chart/index.html
diff --git a/gui-reference/concrete-simulator/simulation-control/index.html b/gui-reference/concrete-simulator/simulation-control/index.html
diff --git a/gui-reference/concrete-simulator/variables/index.html b/gui-reference/concrete-simulator/variables/index.html
diff --git a/gui-reference/index.html b/gui-reference/index.html
diff --git a/gui-reference/menu-bar/edit/index.html b/gui-reference/menu-bar/edit/index.html
diff --git a/gui-reference/menu-bar/file/index.html b/gui-reference/menu-bar/file/index.html
diff --git a/gui-reference/menu-bar/help/index.html b/gui-reference/menu-bar/help/index.html
diff --git a/gui-reference/menu-bar/index.html b/gui-reference/menu-bar/index.html
diff --git a/gui-reference/menu-bar/options/index.html b/gui-reference/menu-bar/options/index.html
diff --git a/gui-reference/menu-bar/tools/index.html b/gui-reference/menu-bar/tools/index.html
diff --git a/gui-reference/menu-bar/view/index.html b/gui-reference/menu-bar/view/index.html
diff --git a/gui-reference/symbolic-simulator/index.html b/gui-reference/symbolic-simulator/index.html
diff --git a/gui-reference/symbolic-simulator/process/index.html b/gui-reference/symbolic-simulator/process/index.html
diff --git a/gui-reference/symbolic-simulator/sequence-charts/index.html b/gui-reference/symbolic-simulator/sequence-charts/index.html
diff --git a/gui-reference/symbolic-simulator/simulation-control/index.html b/gui-reference/symbolic-simulator/simulation-control/index.html
diff --git a/gui-reference/symbolic-simulator/symbolic-traces/index.html b/gui-reference/symbolic-simulator/symbolic-traces/index.html
diff --git a/gui-reference/symbolic-simulator/variables/index.html b/gui-reference/symbolic-simulator/variables/index.html
diff --git a/gui-reference/system-editor/declarations/index.html b/gui-reference/system-editor/declarations/index.html
diff --git a/gui-reference/system-editor/drawing/index.html b/gui-reference/system-editor/drawing/index.html
diff --git a/gui-reference/system-editor/index.html b/gui-reference/system-editor/index.html
diff --git a/gui-reference/system-editor/navigation-tree/index.html b/gui-reference/system-editor/navigation-tree/index.html
diff --git a/gui-reference/toolbar/index.html b/gui-reference/toolbar/index.html
diff --git a/gui-reference/verifier/index.html b/gui-reference/verifier/index.html
diff --git a/gui-reference/verifier/specifying/index.html b/gui-reference/verifier/specifying/index.html
diff --git a/gui-reference/verifier/verifying/index.html b/gui-reference/verifier/verifying/index.html
diff --git a/gui-reference/yggdrasil/index.html b/gui-reference/yggdrasil/index.html
diff --git a/gui-reference/yggdrasil/test-code/index.html b/gui-reference/yggdrasil/test-code/index.html
diff --git a/gui-reference/yggdrasil/traces/index.html b/gui-reference/yggdrasil/traces/index.html
diff --git a/gui-reference/yggdrasil/tutorial/basic-test-generation/index.html b/gui-reference/yggdrasil/tutorial/basic-test-generation/index.html
diff --git a/gui-reference/yggdrasil/tutorial/index.html b/gui-reference/yggdrasil/tutorial/index.html
diff --git a/gui-reference/yggdrasil/tutorial/using-queries/index.html b/gui-reference/yggdrasil/tutorial/using-queries/index.html
diff --git a/gui-reference/yggdrasil/tutorial/using-variables/index.html b/gui-reference/yggdrasil/tutorial/using-variables/index.html
diff --git a/index.html b/index.html
diff --git a/index.json b/index.json
diff --git a/index.xml b/index.xml
@@ -36,11 +36,10 @@ SMCQuery ::= Simulate Subjection | Probability Subjection | ProbUntil Subjection
 The first group contains the following buttons: New, Open Project, and Save. These features are described in the File menu section.</description></item><item><title>Variables Panel</title><link>/gui-reference/concrete-simulator/variables/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/gui-reference/concrete-simulator/variables/</guid><description>The variables panel is the middle panel of the simulator. It displays the values of the data and clock variables in the current state or transition selected in the trace of the simulation control panel.</description></item><item><title>Verifying Requirements</title><link>/gui-reference/verifier/verifying/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/gui-reference/verifier/verifying/</guid><description>The queries (i.e. the system requirements) are verified from the verifier interface of UPPAAL. A verification is always performed according to the settings specified in the Options menu of the main menu bar.
 The selected queries are verified when the button named Check is pressed. The verification progress dialog displays the progress of how many queries have been verified, what is the current load of a passed-waiting list, current processor time usage (the time spent for verification is in blue, the time spent by operating system is in red), current usage of host&amp;rsquo;s random access memory (verification memory is in blue, memory used by other running processes is in gray and operating system cache and buffers are in yellow), swap disk usage (swapped out verification is in blue, other is in grey).</description></item><item><title>verifyta</title><link>/toolsandapi/verifyta/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/toolsandapi/verifyta/</guid><description>The verifier functionality is accessible through verifyta command line utility in bin-Windows or bin-Linux directory of the distribution. The supported options are displayed when running verifyta -h.</description></item><item><title>Syntax of Learning Queries</title><link>/language-reference/query-syntax/learning_queries/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/language-reference/query-syntax/learning_queries/</guid><description>Learning Queries LearningQuery ::= ExpQuantifier &amp;#39;(&amp;#39; Expression &amp;#39;)&amp;#39; &amp;#39;[&amp;#39; BoundType &amp;#39;]&amp;#39; Features? &amp;#39;:&amp;#39; PathType Expression Subjection | ExpQuantifier &amp;#39;[&amp;#39; BoundType &amp;#39;]&amp;#39; Features? &amp;#39;:&amp;#39; PathType Expression Subjection | ExpPrQuantifier &amp;#39;[&amp;#39; BoundType &amp;#39;]&amp;#39; Features? &amp;#39;:&amp;#39; PathType Expression Subjection ExpQuantifier ::= ( minE | maxE ) ExpPrQuantifier ::= ( minPr | maxPr ) Features ::= &amp;#39;{&amp;#39; List &amp;#39;}&amp;#39; &amp;#39;-&amp;gt;&amp;#39; &amp;#39;{&amp;#39; List &amp;#39;}&amp;#39; Subjection ::= // empty for no subjection | under StrategyName Features describes a mapping (state space partition) from a partial state to a player action.</description></item><item><title>Declarations</title><link>/gui-reference/system-editor/declarations/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/gui-reference/system-editor/declarations/</guid><description>Types, constants, variables and functions can be defined in the global scope by placing them in the global section labelled Declarations or System declarations, or locally for a template by placing in the Declarations section of a template.
 Processes are instantiated by placing a process assignments in the System declarations section.
-Finally, the system is defined as a parallel composition of a number of processes by placing a system declaration in the System declarations section.</description></item><item><title>External Functions</title><link>/language-reference/system-description/declarations/external-functions/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/language-reference/system-description/declarations/external-functions/</guid><description>External Functions is an expert user feature and requires a high-level understanding of dynamic library loading and linking.
+Finally, the system is defined as a parallel composition of a number of processes by placing a system declaration in the System declarations section.</description></item><item><title>External Functions</title><link>/language-reference/system-description/declarations/external-functions/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/language-reference/system-description/declarations/external-functions/</guid><description>The external functions are supported since Uppaal Stratego version 4.1.20-7, or Uppaal version 5.0 or later.
+External Functions is an expert user feature and requires a high-level understanding of dynamic library loading and linking.
 The feature is supported on Linux and experimental on Windows and macOS.
-This feature is supported since Uppaal Stratego version 4.1.20-7, or Uppaal version 5.0 or later.
-External Functions can be declared alongside other declaratios. External functions are local to the current scope, defined by the grammar:
-ExternDecl = &amp;#39;import&amp;#39; Path &amp;#39;{&amp;#39; [FwdDeclList] &amp;#39;}&amp;#39; FwdDeclList = FwdDecl &amp;#39;;&amp;#39; | FwdDeclList FwdDecl &amp;#39;;&amp;#39; FwdDecl = [ID &amp;#39;=&amp;#39;] Type ID &amp;#39;(&amp;#39; [Parameters] &amp;#39;)&amp;#39; Path is a double-quoted (using &amp;quot;) character sequence (string) denoting a file path to the library placed on the same computer as the used engine (server or verifyta).</description></item><item><title>Gantt Chart</title><link>/language-reference/system-description/system-definition/gantt-chart/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/language-reference/system-description/system-definition/gantt-chart/</guid><description>A Gantt chart, commonly used in project management, is a bar chart that shows activities displayed against time. On the left of the chart is a list of the activities and along the top is a suitable time scale. Each activity is represented by a bar; the position and length of the bar reflect the start date, duration and end date of the activity.
+The external function calls must be deterministic: for any argument values, the function should produce the same result at any time when called with the same values.</description></item><item><title>Gantt Chart</title><link>/language-reference/system-description/system-definition/gantt-chart/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/language-reference/system-description/system-definition/gantt-chart/</guid><description>A Gantt chart, commonly used in project management, is a bar chart that shows activities displayed against time. On the left of the chart is a list of the activities and along the top is a suitable time scale. Each activity is represented by a bar; the position and length of the bar reflect the start date, duration and end date of the activity.
 In UPPAAL Gantt Charts are used to automatic visualize traces in Concrete Simulator.</description></item><item><title>Java API</title><link>/toolsandapi/javaapi/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/toolsandapi/javaapi/</guid><description>UPPAAL models can be created, loaded, saved, simulated and checked using libs/model.jar library. There is also javadoc included libs/model-javadoc.jar.
 A demonstrating example is included in the demo/ModelDemo.java file.</description></item><item><title>Parameters</title><link>/language-reference/system-description/parameters/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/language-reference/system-description/parameters/</guid><description>Templates and functions are parameterised. The syntax for parameters is defined by the grammar for Parameters:
 Parameters ::= [ Parameter (&amp;#39;,&amp;#39; Parameter)* ] Parameter ::= [Type] [ &amp;#39;&amp;amp;&amp;#39; ] [ID] [ArrayDecl]* In contrast to global and local declarations, the parameter list should not be terminated by a semicolon.