{"id":249,"date":"2013-04-18T18:05:52","date_gmt":"2013-04-18T16:05:52","guid":{"rendered":"https:\/\/project.inria.fr\/pyecdar\/?page_id=249"},"modified":"2013-04-18T21:46:31","modified_gmt":"2013-04-18T19:46:31","slug":"adaptive-system-tutorial","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/pyecdar\/adaptive-system-tutorial\/","title":{"rendered":"Adaptive system tutorial"},"content":{"rendered":"

Inside the python shell:
\nLoading the tool<\/strong>:<\/strong><\/p>\n

from pyecdar import loadModel<\/code><\/p>\n

Loading the model into the workspace:\u00a0<\/strong><\/p>\n

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<\/a>.<\/p>\n

W = loadModel(\"routing_protocol.xml\")<\/code><\/p>\n

Load a timed game associated to a template:<\/strong><\/p>\n

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.<\/a><\/p>\n

G = W.getTimedGame(\"Protocol\", \"A[]([not safe] not RoutedSafe)\")<\/code><\/p>\n

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.<\/p>\n

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

Therefore this property is satisfied in three conditions:<\/p>\n