Adaptive system tutorial

Inside the python shell:
Loading the tool:

from pyecdar import loadModel

Loading the model into the workspace: 

Choose a workspace name (for instance W), and load a UPPAAL model from an XML file. We load the routing protocol model described in the example section.

W = loadModel("routing_protocol.xml")

Load a timed game associated to a template:

A UPPAAL model file generated may contain several templates, each described by Timed Input/Output Automata (TIOA) or Feature Timed Game Automata (FTGA). Each template defines a timed specification or timed game that can be loaded inside the shell and assign to a variable. For timed games we need to provide a T-AdaCTL formula.

G = W.getTimedGame("Protocol", "A[]([not safe] not RoutedSafe)")

This creates a game structure composed by a FTGA and a T-AdaCTL formula on which the user can performs analysis. The formula checks that whenever the environment is not safe, then the protocol is not in the RoutedSafe location.

To solve the game the user launch the command G.solve(). This prints as a results the sets of features that allow to win the game from the initial state:
Checking formula 'A[]([not Fe[0]] not RoutedSafe)' in template 'Protocol'
=== Winning features ===
(not preconf and not treconf and encrypt) or (not preconf and treconf) or (preconf)

Therefore this property is satisfied in three conditions:

  • when the adaptive features encrypt is enable
  • when the system treconf is enable
  • when the system preconf is enable

Additionaly the user can extract a BDD with the sets of winning features:

G.get_winning_features()

This returns an object from the PyCUDD library that can be used for further analysis.

Another timed game:

G = pytiga.TimedGame(P,"A[]([safe] not Received or (A<>[0,20](Ready)))")

The formula means that if the environment is safe in location Received then the location Ready is reached within 20 time units.

G.solve()
Checking formula 'A[]([safe] not Received or (A<>[0,20](Ready)))' in template 'Protocol'
=== Winning features ===
(~preconf and ~encrypt) or (preconf)
This property is only satisfied if the system feature preconf is enable, or if the adaptive feature encrypt is initially disable.

A third game:

G = pytiga.TimedGame(P,"A[](([not safe] not RoutedSafe) and ([safe] not Received or (A<>[0,20](Ready))))")

The formula is a combination of the two previous objectives.

G.solve()
Checking formula 'A[](([not safe] not RoutedSafe) and ([safe] not Received or (A<>[0,20](Ready))))' in template 'Protocol'
=== Winning features ===
(preconf)

The results shows that this property is only satisfied if the system feature preconf is enable.