s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

imported patch activate-ltl-step-bounds.patch

tud-infrastructure-2018-10-12
Joachim Klein 7 years ago
parent
0038984be4
commit
c70db33e06
6 changed files with 45 additions and 71 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      prism-tests/bugfixes/supersimple.pm.boundedltl.props
  2. 81
      prism/src/automata/LTL2DA.java
  3. 2
      prism/src/automata/LTL2RabinLibrary.java
  4. 9
      prism/src/explicit/LTLModelChecker.java
  5. 9
      prism/src/prism/LTLModelChecker.java
  6. 5
      prism/src/prism/ProbModelChecker.java

10
prism-tests/bugfixes/supersimple.pm.boundedltl.props
View File

@ -8,12 +8,12 @@ P>=1 [ F<=1 P>0 [ X F "a" ] ]
// RESULT: true
P>0.5 [ F>=1 P>0 [ X F "a" ] ]
// These ones *should* fail for now
// since there is no support for timed LTL currently
// These ones are now supported
// as well
// RESULT: Error "not supported"
// RESULT: true
P>0.5 [ X F P>0 [ X F<=4 "a" ] ]
// RESULT: Error "not supported"
// RESULT: true
P>0.5 [ X F<=1 P>0 [ X F "a" ] ]
// RESULT: Error "not supported"
// RESULT: true
P>0.5 [ X F P>0 [ X F<=1 "a" ] ]

81
prism/src/automata/LTL2DA.java
View File

@ -49,6 +49,7 @@ import jltl2ba.LTLFragments;
import jltl2dstar.LTL2Rabin;
import parser.Values;
import parser.ast.Expression;
import parser.visitor.ExpandStepBoundsSyntactically;
import parser.ast.ExpressionHOA;
import parser.ast.ExpressionLabel;
import parser.ast.ExpressionUnaryOp;
@ -102,9 +103,6 @@ public class LTL2DA extends PrismComponent
boolean useExternal = useExternal();
boolean containsTemporalBounds = Expression.containsTemporalTimeBounds(ltl);
if (containsTemporalBounds) {
useExternal = false;
}
if (!useExternal) {
try {
@ -114,51 +112,50 @@ public class LTL2DA extends PrismComponent
getLog().println("Taking "+result.getAutomataType()+" from library...");
}
} catch (Exception e) {
if (containsTemporalBounds) {
// there is (currently) no other way to translate LTL with temporal bounds,
// so treat an exception as a "real" one
throw e;
} else {
// there is the possibility that we might be able to construct
// an automaton below, just issue a warning
getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:");
getLog().println(" " + e.getMessage());
}
// there is the possibility that we might be able to construct
// an automaton below, just issue a warning
getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:");
getLog().println(" " + e.getMessage());
}
}
if (result == null) {
if (!containsTemporalBounds) {
if (useExternal) {
result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
} else {
SimpleLTL simpleLTL = ltl.convertForJltl2ba();
// don't use LTL2WDBA translation yet
boolean allowLTL2WDBA = false;
if (allowLTL2WDBA) {
LTLFragments fragments = LTLFragments.analyse(simpleLTL);
mainLog.println(fragments);
if (fragments.isSyntacticGuarantee() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.REACH)) {
// a co-safety property
mainLog.println("Generating DFA for co-safety property...");
LTL2WDBA ltl2wdba = new LTL2WDBA(this);
result = ltl2wdba.cosafeltl2dfa(simpleLTL);
} else if (allowLTL2WDBA && fragments.isSyntacticObligation() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.BUCHI)) {
// an obligation property
mainLog.println("Generating DBA for obligation property...");
LTL2WDBA ltl2wdba = new LTL2WDBA(this);
result = ltl2wdba.obligation2wdba(simpleLTL);
}
}
if (result == null) {
// use jltl2dstar LTL2DA
result = LTL2Rabin.ltl2da(simpleLTL, allowedAcceptance);
if (containsTemporalBounds) {
// remove time bounds syntactically
ExpandStepBoundsSyntactically visitor = new ExpandStepBoundsSyntactically(constants);
ltl = (Expression)ltl.deepCopy().accept(visitor);
mainLog.println("LTL formula with syntactically expanded bounds: "+ltl);
}
if (useExternal) {
result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
} else {
SimpleLTL simpleLTL = ltl.convertForJltl2ba();
// don't use LTL2WDBA translation yet
boolean allowLTL2WDBA = false;
if (allowLTL2WDBA) {
LTLFragments fragments = LTLFragments.analyse(simpleLTL);
mainLog.println(fragments);
if (fragments.isSyntacticGuarantee() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.REACH)) {
// a co-safety property
mainLog.println("Generating DFA for co-safety property...");
LTL2WDBA ltl2wdba = new LTL2WDBA(this);
result = ltl2wdba.cosafeltl2dfa(simpleLTL);
} else if (allowLTL2WDBA && fragments.isSyntacticObligation() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.BUCHI)) {
// an obligation property
mainLog.println("Generating DBA for obligation property...");
LTL2WDBA ltl2wdba = new LTL2WDBA(this);
result = ltl2wdba.obligation2wdba(simpleLTL);
}
}
} else {
throw new PrismNotSupportedException("Could not convert LTL formula to deterministic automaton, formula had time-bounds");
if (result == null) {
// use jltl2dstar LTL2DA
result = LTL2Rabin.ltl2da(simpleLTL, allowedAcceptance);
}
}
}

2
prism/src/automata/LTL2RabinLibrary.java
View File

@ -160,7 +160,7 @@ public class LTL2RabinLibrary
// handle simple until formula with time bounds
if (Expression.containsTemporalTimeBounds(ltl)) {
if (!ltl.isSimplePathFormula()) {
throw new PrismNotSupportedException("Unsupported LTL formula with time bounds: "+ltl);
return null;
}
ltl = Expression.convertSimplePathFormulaToCanonicalForm(ltl);

9
prism/src/explicit/LTLModelChecker.java
View File

@ -135,11 +135,6 @@ public class LTLModelChecker extends PrismComponent
// Only support temporal bounds for discrete time models
return false;
}
if (!expr.isSimplePathFormula()) {
// Only support temporal bounds for simple path formulas
return false;
}
}
if (Expression.isHOA(expr))
@ -239,10 +234,6 @@ public class LTLModelChecker extends PrismComponent
if (model.getModelType().continuousTime()) {
throw new PrismNotSupportedException("Automaton construction for time-bounded operators not supported for " + model.getModelType()+".");
}
if (!expr.isSimplePathFormula()) {
throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
}
}
if (Expression.isHOA(expr)) {

9
prism/src/prism/LTLModelChecker.java
View File

@ -177,11 +177,6 @@ public class LTLModelChecker extends PrismComponent
// Only support temporal bounds for discrete time models
return false;
}
if (!expr.isSimplePathFormula()) {
// Only support temporal bounds for simple path formulas
return false;
}
}
if (Expression.isHOA(expr)) {
@ -326,10 +321,6 @@ public class LTLModelChecker extends PrismComponent
if (model.getModelType().continuousTime()) {
throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
}
if (!expr.isSimplePathFormula()) {
throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
}
}
long time;

5
prism/src/prism/ProbModelChecker.java
View File

@ -1023,11 +1023,6 @@ public class ProbModelChecker extends NonProbModelChecker
JDD.Deref(statesOfInterest);
throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
}
if (!expr.isSimplePathFormula()) {
JDD.Deref(statesOfInterest);
throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
}
}
// Can't do "dfa" properties yet

Write Preview
Loading…
Cancel
Save