(CTMC-LTL) FragmentSpecification: cslstar and csrlstar

Conflicts:
	src/storm/logic/FragmentSpecification.cpp
	src/storm/logic/FragmentSpecification.h

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();
 

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();