From 9bfb1fedc247618fb1e3b54538dc74b80169dcce Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 11 Jul 2017 14:48:54 +0200
Subject: [PATCH] requiring that multi objective queries have a multi(..)
formula at top level.
---
src/storm/logic/FragmentChecker.cpp | 3 +++
src/storm/logic/FragmentSpecification.cpp | 11 +++++++++++
src/storm/logic/FragmentSpecification.h | 4 ++++
.../csl/SparseMarkovAutomatonCslModelChecker.cpp | 4 ++--
.../modelchecker/prctl/SparseMdpPrctlModelChecker.cpp | 4 ++--
5 files changed, 22 insertions(+), 4 deletions(-)
diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp
index ee0967d22..6fc458796 100644
--- a/src/storm/logic/FragmentChecker.cpp
+++ b/src/storm/logic/FragmentChecker.cpp
@@ -24,6 +24,9 @@ namespace storm {
if (specification.isOperatorAtTopLevelRequired()) {
result &= f.isOperatorFormula();
}
+ if (specification.isMultiObjectiveFormulaAtTopLevelRequired()) {
+ result &= f.isMultiObjectiveFormula();
+ }
return result;
}
diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp
index 19c4116aa..11a3ac2f4 100644
--- a/src/storm/logic/FragmentSpecification.cpp
+++ b/src/storm/logic/FragmentSpecification.cpp
@@ -88,6 +88,7 @@ namespace storm {
FragmentSpecification multiObjective = propositional();
multiObjective.setMultiObjectiveFormulasAllowed(true);
+ multiObjective.setMultiObjectiveFormulaAtTopLevelRequired(true);
multiObjective.setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(true);
multiObjective.setProbabilityOperatorsAllowed(true);
multiObjective.setUntilFormulasAllowed(true);
@@ -148,6 +149,7 @@ namespace storm {
quantitativeOperatorResults = true;
operatorAtTopLevelRequired = false;
+ multiObjectiveFormulaAtTopLevelRequired = false;
operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false;
}
@@ -489,6 +491,15 @@ namespace storm {
return *this;
}
+ bool FragmentSpecification::isMultiObjectiveFormulaAtTopLevelRequired() const {
+ return multiObjectiveFormulaAtTopLevelRequired;
+ }
+
+ FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulaAtTopLevelRequired(bool newValue) {
+ multiObjectiveFormulaAtTopLevelRequired = newValue;
+ return *this;
+ }
+
bool FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const {
return operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
}
diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h
index 619394189..74d420f5b 100644
--- a/src/storm/logic/FragmentSpecification.h
+++ b/src/storm/logic/FragmentSpecification.h
@@ -118,6 +118,9 @@ namespace storm {
bool isOperatorAtTopLevelRequired() const;
FragmentSpecification& setOperatorAtTopLevelRequired(bool newValue);
+ bool isMultiObjectiveFormulaAtTopLevelRequired() const;
+ FragmentSpecification& setMultiObjectiveFormulaAtTopLevelRequired(bool newValue);
+
bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const;
FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue);
@@ -170,6 +173,7 @@ namespace storm {
bool quantitativeOperatorResults;
bool qualitativeOperatorResults;
bool operatorAtTopLevelRequired;
+ bool multiObjectiveFormulaAtTopLevelRequired;
bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
};
diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
index 2f90c23d5..1bd826c7f 100644
--- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
+++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
@@ -39,8 +39,8 @@ namespace storm {
} else {
// Check whether we consider a multi-objective formula
// For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states.
- if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
- if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+ if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+ if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
return formula.isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
}
}
diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index 4aaee1400..a40d04f08 100644
--- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -48,8 +48,8 @@ namespace storm {
} else {
// Check whether we consider a multi-objective formula
// For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states.
- if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
- if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+ if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+ if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
}
}