Add license, support, and uppaal mini tutorial.

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2020 Guillermina Cledou, José Proença
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

docs/source/conf.py

@@ -20,8 +20,8 @@
 # -- Project information -----------------------------------------------------
 
 project = 'Hubs for VirtuosoNext™'
-copyright = '2020, arca.di.uminho.pt'
-author = 'arca.di.uminho.pt'
+copyright = '2020, Guillermina Cledou, José Proença '
+author = 'Guillermina Cledou, José Proença'
 
 
 # -- General configuration ---------------------------------------------------
@@ -62,3 +62,5 @@
 ]
 
 
+
+

docs/source/index.rst

@@ -19,11 +19,21 @@ The toolset is developed as a sub-module of `ReoLive <https://github.com/ReoLang
 
 .. toctree::
    :maxdepth: 2
+   :caption: Getting started
    :hidden:
 
-   try-it
    install
+   tutorial
+
+.. toctree::
+   :maxdepth: 2
+   :caption: Resources
+   :hidden:
+
    publications
+   support
+
+
 
 VirtuosoNext™ RTOS
 ==================
@@ -44,4 +54,4 @@ Hubs for VirtuosoNext™ toolset is available to use
 or to download and install locally following the
 :doc:`installation guidelines <install>`.
 
-Either case, read :doc:`try-it` to learn more about how to use the tools.
+Either case, read :doc:`tutorial` to learn more about how to use the tools.

docs/source/support.rst

@@ -0,0 +1,9 @@
+.. _support:
+
+Support
+*******
+
+We are available for support in case you encounter any issue or have trouble using the tools.
+
+- Guillermina Cledou: mgc at inesctec dot pt
+- José Proença: pro at isep dot ipp dot pt

docs/source/try-it.rst → docs/source/tutorial.rst

@@ -256,7 +256,7 @@ Composed hubs with shared port names will synchronize over such ports.
 
     // Main block (Preo Syntax)
     // uses the hub myDupl specified in the code block
-    myHub
+    myDupl
 
     {
         // a hub using Treo syntax
@@ -286,7 +286,7 @@ Various hubs specified inside the block are separated by ``,``.
 
     // Main block (Preo Syntax)
     // uses the hub myDupl specified in the code block
-    timer(5) ; myHub
+    timer(5) ; myDupl
 
     {
         // a hub using Treo syntax
@@ -526,8 +526,7 @@ while ``[]`` and ``<>`` are the universal and existential quantifiers over state
 ``a.t`` is a special clock assigned to port `a` that is set to `0` every time `a` fires -- i.e.,
 after `a` fired, this clock tracks the time since `a` last fired.
 
-The following table describes intuitively when each formuly is satisfied.
-For a formal definition of satisfaction checkout `the technical report  <#>`_.
+The following table describes intuitively when each formula is satisfied.
 
 ========================= =======================================================================
 Construct                      Description
@@ -611,6 +610,27 @@ In particular, for each property, the result box shows:
     Thus, each property has its own Uppaal model.
 
 
+Manual verification using Uppaal
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Although the user can automatically verify properties from the temporal logic widget, as explained above,
+it its possible to download the model |download| and import the model from the Uppaal model checker.
+
+After running Uppaal, go to **File** -> **Open System** and select the ``.xml`` model downloaded either from the
+:ref:`uppaal` or :ref:`temporal-widget` widget.
+
+- **Editor**: shows the automaton of the hub and the structure of the Uppaal Project.
+  Global declarations of variables, clocks, and channels, can be found under *Declarations*, while local declarations
+  can be found under *Hub* -> *Declarations*. The initialization of the system is found under *System declarations*.
+- **Simulator**: provides tools to simulate executions by selecting an enabled transition, while
+  highlighting the current location in the automaton, among other functionality.
+- **Verifier**: provides functionality to write temporal properties and verify them.
+  If the model imported was downloaded from the :ref:`temporal-widget` widget,
+  it will show the corresponding property for which the model was created.
+
+
+.. _uppaal:
+
 Uppaal Model
 ------------
 

readme.md

@@ -22,4 +22,4 @@ Hubs for VirtuosoNext™ toolset is available to use
 or to download and install locally following the
 [installation guidelines](https://hubs.readthedocs.io/en/latest/install.html).
 
-Either way, [read the docs](https://hubs.readthedocs.io/en/latest/try-it.html) to learn more about how to use the tools.
+Either way, [read the docs](https://hubs.readthedocs.io/en/latest/tutorial.html) to learn more about how to use the tools.