Interface Featured Timed Automata
This project is a small Scala implementation of the Interface Featured Timed Automata (IFTA), that will include:
- a small scala DSL
- composition operator of IFTAs
- export into UPPAAL Timed Automata with features
Below you will find a quick overview on how to build, visualise, compose, and analyse IFTA using our Scala library. For more examples, please check our examples folder.
Building primitive IFTAs
To compile and run the tools you can use sbt, for example, by executing the command
There, you can try the following commands:
import ifta.DSL._ val myAut = newifta ++ ( 0 --> 1 by "a,b" when "f", 1 --> 0 by "c" when "g" ) startWith 0 when "g"-->"f" // Create a simple automaton with 2 transitions and initial location "0". // "f" and "g" are features that must obey the constraint "g -> f", and // determine which edges exist. myAut.isValid // returns "true", meaning that the feature model is non-empty (i.e., satisfiable). myAut.instance // or myAut.instance("f") to refine // finds a concrete product (timed automaton), by selecting a valid product and instantiating the automaton.
To debug and analyse automata, three functions are provided to produce an intuitive
dot graph file, an
xml file that can be used by Uppaal, and an interactive
html file using Vis.js to visualize an automata and see how it is affected by its possible feature selections.
toDot(myAut) // outputs the automaton in dot format (for graphviz - https://mdaines.github.io/viz.js) toUppaal(myAut get "a" pub "b,c","myAut.xml") // produces an xml file that can be opened with Uppaal model checker, using "a" as an input channel and "b" and "c" as output channels // the application IFTA is defined in the examples folder toVis(application, "application.html") // produces an html file that can be opened in a browser and see which transitions are enabled in each possible feature selection
dot output is handy to quickly visualise a connector with an intuitive layout (use, for example online tool Viz.js to preview the produced graph).
The Uppaal output requires some manual layout adjustments but can be used to simulate and to prove (temporal) properties.
Note that the
Uppaal model was extended to annotations to make
a an input channel and
c output channels, represented as
c! in the Uppaal model.
html output is handy to see what possible feature selections are derived from the feature model and how they affect the transitions of the automata.
Screenshots of the
Vis.js outputs follow bellow.
Observe that Uppaal does not support multiple actions per transition - these are rewritten as an interleaving of all combinations, imposing that inputs come before outputs (to reduce the state space).
Automata can be extended with clocks, using the same notion of clocks as Uppaal. Hence, states can have clock constraints as invariants, and edges can have clock constraints as guards that make a transition active.
The code below defines a simple coffee machine
cm with 2 features
mk (standing for coffee and milk), and with 3 actions:
ca (cappuccino), and
Time is captured by the clock
c, that is set to 0 every time the automata evolves to location 1, and is used to specify that the coffee will be brewed some time between 2 and 5 time units after selecting the product.
val cm = newifta ++ ( 0 --> 1 by "co" when "cf"&&"mk" reset "c", 0 --> 1 by "ca" when "cf" reset "c", 1 --> 0 by "b" cc "c">=2 ) startWith 0 when "mk"-->"cf" inv(1,"c"<=5) get "co" get "ca" pub "b"
a2 can be composed in 2 ways:
a1 * a2: using the product of IFTA, which returns a new IFTA;
a1 || a2: creating a network of parallel IFTA, without calculating the product.
An example of these compositions follow below, using
sync to rename ports that are connected (and need to be unified.
val cm = ... /* as before */ val rtr = newifta ++ ( 0 --> 1 by "i" when "vi" && ("vo1"||"vo2"), 1 --> 0 by "o1" when "vi" && "vo1", 1 --> 0 by "o2" when "vi" && "vo2" ) startWith 0 get "i" pub "o1" pub "o2" // or simply: val rtr = router("i","o1","o2") // network of 2 automata (communicating over 2 pairs of ports) val netComp = (cm || rtr) sync ("o1"->"ca","o2"->"co") // flattened of the same 2 automata val prodComp = netComp.flatten // same as (cm || rtr) product ("o1"->"ca","o2"->"co") // same as (cm sync ("o1"->"ca","o2"->"co"))*(rtr sync ("o1"->"ca","o2"->"co"))
The automata of
rtr, and the product
prodComp are depicted below, respectively.
Observe that both compositions
prodComp can be exported to Uppaal: the former using a network of automata, and the latter producing a single automaton.
In larger examples it is often necessary to visualise the composition of automata. This can be done, for example, as follows.
con2dot( ((cm name "CM") || (rtr name "Rt")) sync link ) // produces a dot graph depicting how the different IFTA of the network interact // seq3net is a NIFTA for a sequencer connector of three outputs. Its definition can be found in the examples folder con2vis(seq3net, "seq3net.html") // produces a html file depicting how the different IFTA of the network interact // and how the feature selections derived from its feature model affect the precense of intefaces