Benchmarks

The results on this page were obtained with Mcta's abstract distance function hL which is based on the monotonicity abstraction. All results were computed on an Intel Xeon with 2.66 Ghz with Mcta-0.1. All benchmark files can be obtained in the download section. Dashes in the tables indicate out of memory (more than 4 GB). The results were obtained with the following command line options:

A* Search

f(s) = h(s) + depth(s), returns shortest error traces for admissible h

mcta -o3 -h5 -c2
Greedy Search

f(s) = h(s)

mcta -o2 -h5 -c2
Useless Transitions (UT)

f(s) = h(s) + depth(s) if s is reached via a useless transition, h(s) otherwise

mcta -o2 -h6 -c2

States with lower f values are preferred. If you are interested in more information about directed model checking, go here.

Single-tracked Line Segment

The Single-tracked Line Segment study stems from an industrial project partner of the UniForM-project [2] and the problem is to design a distributed real-time controller for a segment of tracks where trams share a piece of track. A distributed controller was modeled in terms of PLC-Automata [2, 3], an automata-like notation for real-time programs. The PLC-Automata were translated into timed automata with the tool Moby/RT [4]. For the evaluation of our approach we choose the property that never both directions are given permission to enter the shared segment simultaneously. This property is ensured by 3 PLC-Automata of the whole controller and we injected an error by manipulating a delay such that the asynchronous communication between these automata is faulty. In Moby/RT abstractions are offered for the translation into the timed automata. The given set of PLC-Automata had eight input variables and we constructed six models with decreasing size by abstracting more and more of these inputs.

explored statesruntime in speak memory in MBtrace length
Exp.A*greedyUTA*greedyUTA*greedyUTA*greedyUT
C1.q22501192816580.30.10.26058585410091
C2.q66791456613330.70.20.26558585413291
C3.q76777600211530.90.20.26659585412891
C4.q7265168113110017.01.40.2130705855344121
C5.q6.00e+643049483355.37.30.261611858561057114
C6.q-4.56e+6833-63.90.3-63259-3217114
C7.q--829--0.4--59--114
C8.q-11.91e+6816-144.30.3-1.4 G59-564495
C9.q-27.74e+613423-326.83.2-3.0 G73-580390

Mutual Exclusion

Mutual Exclusion is a case study that models a real-time protocol to ensure mutual exclusion of a state in a distributed system via asynchronous communication. The protocol is described in full detail in [3]. By increasing an upper time bound in the model we got a flawed specification that we transformed into its timed automata semantics by applying various abstractions techniques. The resulting models do not have many automata but a non-trivial amount of clocks and variables.

explored statesruntime in speak memory in MBtrace length
Exp.A*greedyUTA*greedyUTA*greedyUTA*greedyUT
M1.q34680458142560.20.10.16058584745797
M2.q1350731583281860.90.10.1676159501124146
M3.q1551647655106501.00.10.16759605074891
M4.q58422171033224124.50.50.2967066533381136
N1.q805415086956891.11.50.16896594926053108
N2.q33248630476153775.60.40.3927063521679152
N3.q40690811576163327.50.20.39462655279991
N4.q1.59e+61003364419936.21.20.71889284552455118

Fischer

We use two variants of the Fischer protocol for mutual exclusion, which is well-known and scalable. The test examples are denoted FXi in the tables, where X is A, B and i is the number of parallel automata. The error condition is that at least two of the i automata are in a certain location simultaneously. We made the error possible by weakening one of the temporal conditions in the automata (from "<" to "≤"). The variants differ in the way they encode the error condition (note that we have no disjunction in our language).

Variant A adds additional automata with synchronisation.

explored statesruntime in speak memory in MBtrace length
Exp.A*greedyUTA*greedyUTA*greedyUTA*greedyUT
FA5.q71990.10.00.1575757888
FA10.q511990.10.00.1585757888
FA15.q1701990.10.00.1665757888

Variant B selects and specifies two of the automata for the error condition.

explored statesruntime in speak memory in MBtrace length
Exp.A*greedyUTA*greedyUTA*greedyUTA*greedyUT
FB5.q5417970.00.00.05757576126
FB10.q4298637870.11.50.158162576226
FB15.q1504-70.1-0.167-576-6

Arbiter Tree

This case study models a mutual exclusion protocol based on a tree of binary arbiter processes. Client processes are situated at the leaves of the tree. In order to gain access to the shared resource, they may send a request to their respective parent, which in turn passes the request on to its parent, etc. When the root process of the tree receives a request, it generates a grant which is then propagated back down. When the client is done with the resource, it sends a release signal.

In order to avoid blocking client processes, arbiters need to be ready to receive requests from one of their children even when they are already processing one for the other child. In this case it makes sense to send a grant to the second child as soon as a release is received from the first, instead of first forwarding the release upwards and sending a new request. This can be applied asymmetrically (giving a grant to the left child first, and always forwarding releases from the right child to the parent) in order to not monopolize the resource.

explored statesruntime in speak memory in MBtrace length
Exp.A*greedyUTA*greedyUTA*greedyUTA*greedyUT
A2.q7336150.10.10.1525757122112
A3.q5168206320.20.10.1595858172417
A4.q4.44e+67681195135.010.90.21.2 G11659224222
A5.q-26334634-70.00.3-38163-11227
A6.q--39--1.0--80--32

Valid XHTML 1.0! Valid CSS!