diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 314bca97f..3bd34e629 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -121,6 +121,17 @@ namespace storm { return csl; } + FragmentSpecification cslstar() { + FragmentSpecification cslstar = csl(); + + cslstar.setBinaryBooleanPathFormulasAllowed(true); + cslstar.setUnaryBooleanPathFormulasAllowed(true); + cslstar.setNestedOperatorsAllowed(true); + cslstar.setNestedPathFormulasAllowed(true); + + return cslstar; + } + FragmentSpecification csrl() { FragmentSpecification csrl = csl(); @@ -134,6 +145,19 @@ namespace storm { return csrl; } + FragmentSpecification csrlstar() { + FragmentSpecification csrlstar = cslstar(); + + csrlstar.setRewardOperatorsAllowed(true); + csrlstar.setCumulativeRewardFormulasAllowed(true); + csrlstar.setInstantaneousFormulasAllowed(true); + csrlstar.setReachabilityRewardFormulasAllowed(true); + csrlstar.setLongRunAverageOperatorsAllowed(true); + csrlstar.setTimeBoundedCumulativeRewardFormulasAllowed(true); + + return csrlstar; + } + FragmentSpecification multiObjective() { FragmentSpecification multiObjective = propositional(); diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 8c50c635a..18b8a8686 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -264,9 +264,15 @@ namespace storm { // Regular CSL. FragmentSpecification csl(); + // CSL*, i.e., CSL with LTL path formulas. + FragmentSpecification cslstar(); + // CSL + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification csrl(); + // CSL* + cumulative, instantaneous, reachability and long-run rewards. + FragmentSpecification csrlstar(); + // Multi-Objective formulas. FragmentSpecification multiObjective();