|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
See:
Description
Packages | |
---|---|
de.upb.swt.mcie.formulas | This package implements formulas, which can be state formulas, transition formulas or temporal formulas. |
de.upb.swt.mcie.mc | This package implements models with the corresponding model checking procedures, and the main method for invoking the model checker. |
de.upb.swt.mcie.parser | This package implements a parser and compiler for formulas and models. |
de.upb.swt.mcie.parser.token | This package implements the tokens for the scanner and parser of package
de.upb.swt.mcie.parser . |
de.upb.swt.mcie.robdds | This package implements reduced ordered binary decision diagrams (ROBDDs). |
The purpose of the Model Checking in Education (MCiE) project is to demonstrate the implementation of a symbolic model checker based on ROBDDs. It was implemented by Ekkart Kindler as supplementary material for the students of the course on model checking in the winter term 2003/04 at Paderborn University.
Since this first course, MCiE has been extended and improved when used in other projects and during the course "Advanced Topics on Software Engineering" at Denmark's Technical University.
Since the main purpose of this application was educational, it is not particularly tuned to efficiency, but for a clear structure and a safe usability of the libraries. At some places in the code, comments indicate what could be done for improving efficiency - apart from using a compiled programming language such as C instead of Java.
Context
has been
introduced. Now, all ROBDDs are generated in such a context, in
which the involved variables and all corresponding hash tables are
maintained. This makes it easier to work with different variable sets
with different variable orders at the same time. Moreover, it is easier to
get rid of old nodes and variables: simply delete all references to
the context. As soon as all references to a context (and to ROBDDs from
this context) are deleted, all memory used for this context will be claimed
by the garbage collector fully automatically. Moreover, the hash tables of
each context can be cleared individually
(see clearHashTables()
).
Note that now all operations on ROBDDs
may only be applied to ROBDDs from the same context; otherwise a
corresponding IncorrectUseException
will be thrown. Due to the introduction of the
context, the classes Model
and
Formula
had to be revised
too. Each model is now associated with a context. A formula, however,
does not need to know its context. Only when converting a formula to an
ROBDD, the context must be provided. The context can be
either given implicitly via the model
(toROBDD(Model)
for temporal formulas) or by an explicit parameter
when callig the method
toROBDD(Context)
.
successor(ROBDD)
of version 0.2.x contained some errors, which are now
corrected.
Moreover, the class ChangeSet
and the method
predecessors(ROBDD,ChangeSet)
have been added. This way, the variables that
are not changed by a transition relation need not be explicitly mentioned in
the ROBDD, which significantly reduces the size of the corresponding ROBDD
and the time needed for calculating the predecessors.
Transitionsystem
was introduced, which uses a partitioned transition
relation. This results in a more efficient implementation of the ex method
and altogether in more efficient model checking routines.
Moreover, the class ChangeSet
was
equipped with methods for adding variables individually and a method for
clearing its hash tables. In addition, class
Formula
was equipped with a method
adding all variables that occur primed in a formula to a given change set.
This way, it is easier to calculate the appropriate change sets of a
transition formula.
Moreover, the method
successors(ROBDD,ChangeSet)
are implemented now, which can be used for a more
efficient calculation of the reachable states.
FairModel
implements the procedures for fair model checking. These methods work
for any model (with correctly implemented model checking procedures). So
MCiE supports fair model checking for all implemented models including
Kripke structures and fair transition systems. In order to make this work,
the structure of Model
,
Kripkestructure
, and
Transitionsystem
had to be
slightly changed (fairness conditions are no longer included there).
Corrected a problem with the parser: The scanner returned the literals "and" and "or" as unary operators. Therefore, formulas using these textual operators could not be parsed properly. This problem is fixed now.
Added toString() method for formulas to convert formulas to strings in a naive way (with many parentheses).
Copyright (C) 2009, 2010 Ekkart Kindler, Denmark's Technical University (DTU), eki@imm.dtu.dk
The MCiE project is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; version 2 of the License.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |