Created by Jonas G on 2012-03-08 and last modified on 2012-05-24

Using opaal as the base for doing model checking prototyping of capacity timed automata (CTA), described first http://homes.student.aau.dk/jgroth07/CTA.pdf and later refined http://homes.student.aau.dk/jgroth07/TMCCTA.pdf.

The goal is to start out with a discretized version of CTA and then work on removing as much of the discretization as possible to get as close to the definition of CTA as possible while still being able to do model checking.

The problem with CTA is that it has been proven that the reachability problem for CTA is undecidable for CTA with one clock and two capacity variables. By restricting CTA to be completely discrete we can do verification but it is not yet known how much we need to discretize in order to bypass the undecidability of the reachability.

Get this branch:
bzr branch lp:~d801oldf12/opaal/cta
Members of D801oldf12 can upload to this branch. Log in for directions.

Branch merges

Related bugs

Related blueprints

Branch information


Recent revisions

118. By Søren Larsen on 2012-05-24

Graphical changes to models, no syntactic changes.

117. By Jonas G on 2012-05-24

Stupid stuff

116. By Søren Larsen on 2012-05-24

Changes to graphical representation of models, no changes to the actual models.

115. By Jonas G on 2012-05-19

Fixes in autotests

114. By Jonas G on 2012-05-18

Included one query for AAUSAT in first and second approach

113. By Jonas G on 2012-05-17

Noget Lulz i nogle modeller.

Samt noget grahpics til export

112. By Jonas G on 2012-05-14

Fixed several queries that were faulty. Remember to fix in report

111. By Jonas G on 2012-05-11

Set rate bound now has correct state names

Fixes in all approaches

110. By Jonas G on 2012-05-10

Adjusted test runs.

Removed RVC from fourth (infeasible for some reason)

Added single test for AAUSAT in third (not in fourth yet)

109. By Jonas G on 2012-05-10

Changes in all autotests

Fixes to models. Primarily model errors in RVC.

Changes in interval clocks and successor generator.
Proper comparison with interval clocks and discrete update method for IntervalDiscreteClock

Branch metadata

Branch format:
Branch format 7
Repository format:
Bazaar repository format 2a (needs bzr 1.16 or later)
Stacked on:
This branch contains Public information 
Everyone can see this information.