UPPAAL

https://docs.uppaal.org
Admin
UPPAAL is a tool for modeling, validation and verification of real-time systems based on timed...
Tokens:47,725
Snippets:289
Trust Score:8.8
Update:11 months ago
Show doc for...
Tokens:
Raw
### Start UPPAAL GUI

Source: https://docs.uppaal.org/toolsandapi/docker

Launches the UPPAAL graphical user interface. It can be started via its executable or a JAR file and configured to connect to the remote Docker engine.

```bash
java -jar uppaal.jar

```

--------------------------------

### Start Interactive Docker Container Shell

Source: https://docs.uppaal.org/toolsandapi/docker

Starts a Docker container with an interactive shell, useful for debugging. This command overrides the default entrypoint to launch bash.

```bash
docker run --rm -it --entrypoint /bin/bash uppaal-5.0.0

```

--------------------------------

### UPPAAL Dockerfile

Source: https://docs.uppaal.org/toolsandapi/docker

Defines the environment for the UPPAAL Docker image. It sets up a user, installs updates, copies UPPAAL, configures the PATH, and prepares the socket server for remote connections.

```dockerfile
FROM ubuntu:latest

RUN useradd -ms /bin/bash uppaal
RUN apt-get -qq update && apt-get -qq upgrade
USER uppaal
ENV USER=uppaal
WORKDIR /home/uppaal
ADD . uppaal
ENV PATH="/home/uppaal/uppaal/bin:$PATH"
ARG KEY=""
ARG LEASE="1"
RUN verifyta.sh --key ${KEY} --lease ${LEASE}
RUN verifyta.sh --version

EXPOSE 2350
CMD /home/uppaal/uppaal/bin/socketserver.sh /home/uppaal/uppaal/bin/server.sh

```

--------------------------------

### UPPAAL Learning Query Examples

Source: https://docs.uppaal.org/language-reference/query-syntax/learning_queries

Illustrates the usage of learning queries in UPPAAL with practical examples. These examples demonstrate how to specify objectives like minimizing cost or maximizing gain under different observability conditions and time bounds.

```UPPAAL Query Examples
`minE(cost) [<=10] : <> goal`
    learns a strategy that minimizes the expected`cost` expression within `10` time units or when `goal` predicate becomes true given that the **entire** system state is observable.

`maxE(gain) [<=10] : <> goal`
    learns a strategy that maximizes the expected `gain` expression withing `10` time units or when `goal` predicate becomes true.
The `goal` predicate is deprecated, for best results use a predicate which stops together with the simulation bound, like `t>=10`, where `t` is a clock that is never reset.

`minE(cost) [<=10] { i, j } -> { d, f } : <> goal`
    learns a strategy that minimizes the expected `cost` expression within `10` time units or when `goal` predicate becomes true. Where only the expressions `i`, `j`, `d` and `f` are observable. The `{..} -> {..}` syntax controls what is observable. On one hand, by observing only a partial state learning times can be significantly reduced and the strategy structure simplified. On the other hand, the resulting strategy is not guaranteed to converge to a optimal solution under partial observability. There are two types of observable state expressions: _discrete_ and _continuous_. The _discrete_ are specified in the first bracket and the _continuous_ in the second: `{discrete expressions} -> {continuous expressions}`. By default the entire state is considered during learning.
**Discrete** expressions are observed as they are, i.e the query `minE(cost) [<=10] { i, j } -> { } : <> goal` creates a strategy by only observing the values of `i` and `j`.
**Continuous** expressions are discretized using online partition refinement (see Teaching Stratego to Play Ball). The query `minE(cost) [<=10] { } -> { d, f } : <> goal` learns a strategy based on the discretized expressions `d` and `f`.
Integers, clocks, floating points or even arbitrary expressions can be used in either type of observabilty. However we suggest caution when using floating point numbers or clocks in discrete observability.  
Process locations are ignored when specifying observability unless explicitly specified using `location` keyword. For example `Cat.location` and `Mouse.location` refer to the locations of `Cat` and `Mouse` processes.
The learning queries are usually used together with strategy assignment and refinement explained in Strategy Queries.

```

--------------------------------

### Install Docker on Debian/Ubuntu

Source: https://docs.uppaal.org/toolsandapi/docker

Installs the Docker engine on Debian or Ubuntu-based Linux distributions. This is a prerequisite for using Docker to containerize UPPAAL.

```bash
sudo apt install docker.io

```

--------------------------------

### Define Test Case Prefix and Postfix Code (Uppaal System Declarations)

Source: https://docs.uppaal.org/gui-reference/yggdrasil/tutorial/basic-test-generation

Use multi-line comments starting with `TEST_PREFIX` and `TEST_POSTFIX` in the System declarations section to provide wrapper code for each generated test case. This example shows Java class wrapping.

```java
/** TEST_PREFIX
  package app;
  import app.App;

  class Test extends App {

  public static void main(String[] args) {

*/

/** TEST_POSTFIX
  }
}
*/

```

--------------------------------

### Get UPPAAL Version

Source: https://docs.uppaal.org/toolsandapi/docker

Checks the installed UPPAAL version using the verifyta command-line tool. This can help diagnose compatibility issues.

```bash
verifyta --version

```

--------------------------------

### UPPAAL Symbolic Query Examples

Source: https://docs.uppaal.org/language-reference/query-syntax/symbolic_queries

Illustrates various types of symbolic queries with practical examples. These examples cover invariant checks, reachability, implications, and queries for suprema, infima, and bounds.

```uppaal-query
A[] 1<2

```

```uppaal-query
E<> p1.cs and p2.cs

```

```uppaal-query
A[] p1.cs imply not p2.cs

```

```uppaal-query
A[] not deadlock

```

```uppaal-query
sup: Train(1).x, Train(2).x

```

```uppaal-query
sup{Train(1).Crossing}: Train(1).x

```

```uppaal-query
inf{Gate.Occ}: Gate.len

```

```uppaal-query
bounds{Train(1).Crossing}: Train(1).x

```

--------------------------------

### UPPAAL System Definition Example

Source: https://docs.uppaal.org/language-reference/system-description/system-definition

An example demonstrating the textual syntax for defining processes and a system in UPPAAL. This illustrates how templates are declared and instantiated.

```UPPAAL
process P()
{
    state s...;
    ...
}

process Q(int[0,3] a)
{
    state t...;
    ...
}

system P, Q;

```

--------------------------------

### List Installed Docker Images

Source: https://docs.uppaal.org/toolsandapi/docker

Displays all Docker images currently stored on the local machine. This command is useful for verifying that an image has been removed or to see available images.

```bash
docker images

```

--------------------------------

### Example Channel Priority Declaration

Source: https://docs.uppaal.org/language-reference/system-description/priorities

An example demonstrating the declaration of channel priorities. It shows how to assign different priority levels to channels and specific channel instances using the '<' and 'default' keywords.

```uppaal
chan a,b,c,d[2],e[2];
chan priority a,d[0] < default < b,e;
```

--------------------------------

### Get Host C Library Version

Source: https://docs.uppaal.org/toolsandapi/docker

Inspects the host system's C library (libc6) version. This command helps compare the host's C library with the one used by UPPAAL for troubleshooting.

```bash
dpkg -l libc6
dpkg -S libc.so.6
/usr/lib/x86_64-linux-gnu/libc.so.6 --version

```

--------------------------------

### Uppaal Clock Variable Declaration Example

Source: https://docs.uppaal.org/language-reference/system-description/declarations

Example of declaring clock variables.

```text
clock x, y;
```

--------------------------------

### Uppaal Urgent Channel Declaration Example

Source: https://docs.uppaal.org/language-reference/system-description/declarations

Example of declaring an urgent channel, which forces immediate transition when enabled.

```text
urgent chan e;
```

--------------------------------

### Define Test Case Postfix Code (Java Example)

Source: https://docs.uppaal.org/gui-reference/yggdrasil/test-code

Illustrates how to define the postfix code for test cases using a special multi-line comment. This code is executed at the end of each test case. The example completes the Java class structure started in the prefix code.

```UPPAAL System Declaration
/** TEST_POSTFIX
    }
  }
  */
```

--------------------------------

### Get UPPAAL Standard C Library Version

Source: https://docs.uppaal.org/toolsandapi/docker

Retrieves the version of the standard C library used by UPPAAL. This is helpful for understanding library dependencies and potential version conflicts.

```bash
verifyta --stdc-version

```

--------------------------------

### Strategy Query Examples

Source: https://docs.uppaal.org/language-reference/query-syntax/strategy_queries

Illustrates various use cases for strategy queries, including computing and storing a safety strategy, checking conditions under a stored strategy, refining strategies with cost minimization, saving strategies to a file, and loading strategies from a file.

```UPPAAL Query Examples
strategy Safe = A[] safe
A[] good under Safe
E<> goal under Safe
strategy SafeCheap = minE(cost)[<=10] {i,j} -> {d,f} : <> t>=10 under Safe
saveStrategy("folder/file.json", Safe)
strategy Safe = loadStrategy{i,j}->{d,f}("folder/file.json")
```

--------------------------------

### List All Docker Containers (Running and Stopped)

Source: https://docs.uppaal.org/toolsandapi/docker

Shows all Docker containers on the system, including those that have been stopped. This helps in managing and cleaning up containers.

```bash
docker ps -a

```

--------------------------------

### Uppaal Channel Variable Declaration Example

Source: https://docs.uppaal.org/language-reference/system-description/declarations

Example of declaring a standard channel variable.

```text
chan d;
```

--------------------------------

### UPPAAL Location Invariants Examples

Source: https://docs.uppaal.org/language-reference/system-description/templates/locations

Examples of valid invariants for locations in UPPAAL, demonstrating constraints on clocks, clock differences, and clock arrays. It also shows how to set clock rates/derivatives.

```UPPAAL
x <= 2
x < y
forall(i:int[0,2]) x[i] <= 3
forall(i:int[0,2]) y[i]' == b[i]
```

--------------------------------

### Uppaal Struct Declaration and Initialization Example

Source: https://docs.uppaal.org/language-reference/system-description/declarations

Example of declaring a structure with integer and boolean members and initializing it.

```text
struct { int a; bool b; } s1 = { 2, true };
```

--------------------------------

### Uppaal Multidimensional Array with Initializer Example

Source: https://docs.uppaal.org/language-reference/system-description/declarations

Example of a multidimensional integer array with default range and an initializer list for its elements.

```text
int a[2][3] = { { 1, 2, 3 }, { 4, 5, 6} };
```

--------------------------------

### Uppaal Integer Variable with Range and Initializer Example

Source: https://docs.uppaal.org/language-reference/system-description/declarations

Example of an integer variable declared with a specific range and initialized to a value.

```text
int[0,100] a=5;
```

--------------------------------

### UPPAAL Gantt Chart: Scheduling Example

Source: https://docs.uppaal.org/language-reference/system-description/system-definition/gantt-chart

Provides an example of a Gantt chart specification for a scheduling system. It maps different states of a 'Task' (Ready, Running, Blocked, Error) and semaphore usage to integer values representing colors.

```UPPAAL
gantt {
  Task(i : pid_t): Task(i).Ready -> 1,
                   Task(i).Running -> 2,
                   Task(i).Blocked -> 3,
                   Task(i).Error -> 0,
                   for(j : sid_t) Task(i).sema[j] -> 6;
  Scheduler: len==0 -> 0, len>0 -> 1;
}
```

--------------------------------

### Define Test Case Prefix Code (Java Example)

Source: https://docs.uppaal.org/gui-reference/yggdrasil/test-code

Shows how to define the prefix code for test cases using a special multi-line comment. This code is executed at the beginning of each test case. The example provides a Java class structure for a test case.

```UPPAAL System Declaration
/** TEST_PREFIX
  public class Test {
    public static int main(String[] args){
  */
```

--------------------------------

### Remove Docker Container

Source: https://docs.uppaal.org/toolsandapi/docker

Removes a stopped Docker container. This is often used for cleanup, especially if the container was not started with the `--rm` flag.

```bash
docker rm modest_kare

```

--------------------------------

### Build UPPAAL Docker Image

Source: https://docs.uppaal.org/toolsandapi/docker

Builds a Docker image for UPPAAL using the previously created Dockerfile. It allows passing the UPPAAL license key as a build argument.

```bash
cd uppaal-X.Y.Z
docker image build --build-arg KEY=$UPPAAL_LICENSE_KEY --tag uppaal-X.Y.Z -f res/Dockerfile .

```

--------------------------------

### Start UPPAAL Docker Container

Source: https://docs.uppaal.org/toolsandapi/docker

Runs the UPPAAL Docker container in detached mode, mapping port 2350 from the container to the host. The `--rm` flag ensures the container is removed upon stopping.

```bash
docker run --rm -d -p 2350:2350 uppaal-X.Y.Z

```

--------------------------------

### List Running Docker Containers

Source: https://docs.uppaal.org/toolsandapi/docker

Displays a list of currently running Docker containers, including their IDs, images, commands, and port mappings. This is useful for identifying containers to stop or manage.

```bash
docker ps

```

--------------------------------

### UPPAAL Template Instantiation: Partial Instantiation

Source: https://docs.uppaal.org/language-reference/system-description/system-definition/template-instantiation

Illustrates partial instantiation of a UPPAAL template. This allows binding some formal parameters while leaving others free, simplifying the definition of templates with similar arguments. 'Q' is a template with two parameters, and 'Q1', 'Q2' are derived from it.

```UPPAAL
process P(int &x, int y, const int n, const int m)\n{\n    ...\n}\n\nint v, u;\nconst struct { int a, b, c; } data[2] = { { 1, 2, 3 }, { 4, 5, 6 } };\n\nQ(int &x, const int i) = P(x, data[i].a, data[i].b, 2 * data[i].c);\nQ1 = Q(v, 0);\nQ2 = Q(u, 1);\n\nsystem Q1, Q2;\n
```

--------------------------------

### Uppaal Constant Declaration Example

Source: https://docs.uppaal.org/language-reference/system-description/declarations

Example of declaring a constant integer with a specific value.

```text
const int a = 1;
```

--------------------------------

### UPPAAL Update Event Hooks

Source: https://docs.uppaal.org/language-reference/system-description/declarations/functions

Demonstrates syntax for executing statements before and after a transition is taken, using `before_update` and `after_update` blocks. These are useful for capturing state changes.

```UPPAAL
before_update { old_value = variable }
after_update { new_value = variable }

```

--------------------------------

### Example Process Priority Declaration

Source: https://docs.uppaal.org/language-reference/system-description/priorities

Illustrates how to declare priorities for processes within the system declaration line. It uses the '<' separator to indicate higher priority for processes listed to its right, including template sets.

```uppaal
system A < B,C < D;
```

--------------------------------

### Uppaal Boolean Array Declaration Example

Source: https://docs.uppaal.org/language-reference/system-description/declarations

Example of declaring multiple boolean arrays with specified element counts.

```text
bool b[8], c[4];
```

--------------------------------

### Configure Test Case Filename and Extension (Uppaal System Declarations)

Source: https://docs.uppaal.org/gui-reference/yggdrasil/tutorial/basic-test-generation

Optionally, specify custom filenames and file extensions for generated test cases using `TEST_FILENAME` and `TEST_FILEEXT` comments in the System declarations section.

```uppaal
/** TEST_FILENAME test- */
/** TEST_FILEEXT .txt */

```

--------------------------------

### UPPAAL: Initialize Array Function Example

Source: https://docs.uppaal.org/language-reference/system-description/declarations/functions

Initializes an array such that each element holds its corresponding index. Demonstrates call-by-value for array parameters unless an ampersand is used, and uses a range-based for loop.

```UPPAAL
void initialize(int& a[10])
{
    for (i : int[0,9])
    {
        a[i] = i;
    }
}

```

--------------------------------

### UPPAAL Template Instantiation Grammar

Source: https://docs.uppaal.org/language-reference/system-description/system-definition/template-instantiation

This code snippet shows the UPPAAL grammar for template instantiation. It defines how to create a new template based on an existing one, potentially providing arguments for its formal parameters.

```UPPAAL
Instantiation ::= ID [ '(' [Parameters]  ')' ] '=' ID '(' [Arguments] ')' ';'\n
```
Tokens:
Raw