From d1b068eddf7ce81f2a22164501b798a1b8e3be9d Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 13 Jan 2021 12:51:19 +0100 Subject: [PATCH] specified supported rpatl fragment a bit more precisely --- src/storm/logic/FragmentSpecification.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 48b3ac14c..9fd7353b9 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -54,13 +54,15 @@ namespace storm { } 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: Require that operator formulas are required at the top level of a GameFormula? rpatl.setGameFormulasAllowed(true); - + rpatl.setRewardOperatorsAllowed(true); + rpatl.setLongRunAverageRewardFormulasAllowed(true); + rpatl.setLongRunAverageOperatorsAllowed(true); + return rpatl; }