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.
Note that now all operations on ROBDDs may only be applied to ROBDDs from the same context; otherwise a corresponding {@link de.upb.swt.mcie.robdds.IncorrectUseException IncorrectUseException} will be thrown. Due to the introduction of the context, the classes {@link de.upb.swt.mcie.mc.Model Model} and {@link de.upb.swt.mcie.formulas.Formula 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 ({@link de.upb.swt.mcie.formulas.Formula#toROBDD(de.upb.swt.mcie.mc.Model) toROBDD(Model)} for temporal formulas) or by an explicit parameter when callig the method {@link de.upb.swt.mcie.formulas.Formula#toROBDD(Context) toROBDD(Context)}.
Moreover, the class {@link de.upb.swt.mcie.robdds.ChangeSet} and the method {@link de.upb.swt.mcie.robdds.ROBDD#predecessors( de.upb.swt.mcie.robdds.ROBDD, de.upb.swt.mcie.robdds.ChangeSet) 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.
Moreover, the class {@link de.upb.swt.mcie.robdds.ChangeSet ChangeSet} was equipped with methods for adding variables individually and a method for clearing its hash tables. In addition, class {@link de.upb.swt.mcie.formulas.Formula 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 {@link de.upb.swt.mcie.robdds.ROBDD#successors( de.upb.swt.mcie.robdds.ROBDD, de.upb.swt.mcie.robdds.ChangeSet) successors(ROBDD,ChangeSet)} are implemented now, which can be used for a more efficient calculation of the reachable states.
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 @author Ekkart Kindler @version 0.3.7