From 819d97b712f51a271d19c9bee4c2a7a680ff5f83 Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Mon, 24 Aug 2020 22:25:19 +0200
Subject: [PATCH] (CTMC-LTL) FragmentSpecification: cslstar and csrlstar

 Conflicts:
	src/storm/logic/FragmentSpecification.cpp
	src/storm/logic/FragmentSpecification.h
---
 src/storm/logic/FragmentSpecification.cpp | 24 +++++++++++++++++++++++
 src/storm/logic/FragmentSpecification.h   |  6 ++++++
 2 files changed, 30 insertions(+)

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