deploy: 412f01f

UPPAALModelChecker · May 22, 2024 · b980f6a · b980f6a
1 parent 701597a
commit b980f6a
Show file tree

Hide file tree

Showing 85 changed files with 249 additions and 247 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?1716367421 rel=stylesheet><link href=/css/fontawesome-all.min.css?1716367421 rel=stylesheet><link href=/css/hybrid.css?1716367421 rel=stylesheet><link href=/css/featherlight.min.css?1716367421 rel=stylesheet><link href=/css/perfect-scrollbar.min.css?1716367421 rel=stylesheet><link href=/css/theme.css?1716367421 rel=stylesheet><link href=/css/hugo-theme.css?1716367421 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?1716367595 rel=stylesheet><link href=/css/fontawesome-all.min.css?1716367595 rel=stylesheet><link href=/css/hybrid.css?1716367595 rel=stylesheet><link href=/css/featherlight.min.css?1716367595 rel=stylesheet><link href=/css/perfect-scrollbar.min.css?1716367595 rel=stylesheet><link href=/css/theme.css?1716367595 rel=stylesheet><link href=/css/hugo-theme.css?1716367595 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
@@ -34,7 +34,8 @@ Function ::= [Type] [ID] &amp;#39;(&amp;#39; [Parameters] &amp;#39;)&amp;#39; Bl
 If progress measures are defined, UPPAAL uses the generalized sweepline method to reduce the memory usage. However to be efficient, the domain of a progress measure should not be too large - otherwise performance might degrade significantly.</description></item><item><title>Specifying Test Code</title><link>/gui-reference/yggdrasil/test-code/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/gui-reference/yggdrasil/test-code/</guid><description>Traces are translated into executable test cases based on test code entered into the model. The test code is entered as verbatim text, so any language or execution back-end can be used. Test code can be entered in five areas: Prefix code, location enter code, location exit code, edge code, and postfix code. Each test case starts with the prefix code, continues with test code along the locations and edges of the trace and ends with the postfix code.</description></item><item><title>Syntax of Statistical Queries</title><link>/language-reference/query-syntax/statistical_queries/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/language-reference/query-syntax/statistical_queries/</guid><description>Statistical Queries Statistical queries are decided using concrete semantics of stochastic hybrid automata over a number of bounded concrete simulation runs and correspond to empirical measurements of the system performance. The results are of statistical estimate nature and may vary across different executions based on uncertainties specified in Statistical parameters.
 SMCQuery ::= Simulate Subjection | Probability Subjection | ProbUntil Subjection | Probability ( &amp;#39;&amp;lt;=&amp;#39; | &amp;#39;&amp;gt;=&amp;#39; ) PROB Subjection | Probability Subjection &amp;#39;&amp;gt;=&amp;#39; Probability Subjection | Estimate Subjection Simulate ::= &amp;#39;simulate&amp;#39; &amp;#39;[&amp;#39; SMCBounds &amp;#39;]&amp;#39; &amp;#39;{&amp;#39; List &amp;#39;}&amp;#39; [ &amp;#39;:&amp;#39; [ SATRUNS &amp;#39;:&amp;#39; ] Expression ] Probability ::= &amp;#39;Pr&amp;#39; MITLExpression | &amp;#39;Pr[&amp;#39; SMCBounds &amp;#39;]&amp;#39; &amp;#39;(&amp;#39; PathType Expression &amp;#39;)&amp;#39; ProbUntil ::= &amp;#39;Pr[&amp;#39; SMCBounds &amp;#39;]&amp;#39; &amp;#39;(&amp;#39; Expression &amp;#39;U&amp;#39; Expression &amp;#39;)&amp;#39; Estimate ::= &amp;#39;E[&amp;#39; SMCBounds &amp;#39;]&amp;#39; &amp;#39;(&amp;#39; (&amp;#39;min:&amp;#39; | &amp;#39;max:&amp;#39;) Expression &amp;#39;)&amp;#39; SMCBounds ::= BoundType [ ; RUNS ] BoundType ::= ( | Clock | &amp;#39;#&amp;#39; ) &amp;#39;&amp;lt;=&amp;#39; BOUND PathType ::= ( &amp;#39;&amp;lt;&amp;gt;&amp;#39; | &amp;#39;[]&amp;#39; ) Subjection ::= // empty for no subjection | under StrategyName BOUND is a non-negative integer constant denoting an upper bound over the absolute global time (when a variable is not specified), specific Clock (cost) variable or a number of action-transitions (#).</description></item><item><title>Tool Bar</title><link>/gui-reference/toolbar/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>/gui-reference/toolbar/</guid><description>The tool bar is normally located just below the menu bar but can be moved (using the mouse) to other positions or even to a separate window. The tool bar is divided into four groups. The three leftmost groups provide quick access to some of the most frequently used menu items. The rightmost group contains editing tools.
 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.
+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 directory of the UPPAAL distribution.
+The supported options are displayed when running verifyta -h or verifyta --help.</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>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.