Browse Source

specified supported rpatl fragment a bit more precisely

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
d1b068eddf
  1. 6
      src/storm/logic/FragmentSpecification.cpp

6
src/storm/logic/FragmentSpecification.cpp

@ -54,12 +54,14 @@ namespace storm {
} }
FragmentSpecification rpatl() { FragmentSpecification rpatl() {
FragmentSpecification rpatl = prctl();
FragmentSpecification rpatl = propositional();
// TODO: disallow formulas we currently do not support
// TODO: Only allow OperatorFormulas when they are inside of a GameFormula? // TODO: Only allow OperatorFormulas when they are inside of a GameFormula?
// TODO: Require that operator formulas are required at the top level of a GameFormula? // TODO: Require that operator formulas are required at the top level of a GameFormula?
rpatl.setGameFormulasAllowed(true); rpatl.setGameFormulasAllowed(true);
rpatl.setRewardOperatorsAllowed(true);
rpatl.setLongRunAverageRewardFormulasAllowed(true);
rpatl.setLongRunAverageOperatorsAllowed(true);
return rpatl; return rpatl;
} }

Loading…
Cancel
Save