|
|
@ -88,7 +88,7 @@ public class MultiObjModelChecker extends PrismComponent |
|
|
long l = System.currentTimeMillis(); |
|
|
long l = System.currentTimeMillis(); |
|
|
LTL2DA ltl2da = new LTL2DA(this); |
|
|
LTL2DA ltl2da = new LTL2DA(this); |
|
|
dra[i] = ltl2da.convertLTLFormulaToDRA(ltl, modelChecker.getConstantValues()); |
|
|
dra[i] = ltl2da.convertLTLFormulaToDRA(ltl, modelChecker.getConstantValues()); |
|
|
mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getAcceptance().getSizeStatistics() + "."); |
|
|
|
|
|
|
|
|
mainLog.print("DRA has " + dra[i].size() + " states, " + dra[i].getAcceptance().getSizeStatistics() + "."); |
|
|
l = System.currentTimeMillis() - l; |
|
|
l = System.currentTimeMillis() - l; |
|
|
mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds."); |
|
|
mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds."); |
|
|
// If required, export DRA |
|
|
// If required, export DRA |
|
|
|