diff --git a/resources/3rdparty/cudd-3.0.0/Makefile.in b/resources/3rdparty/cudd-3.0.0/Makefile.in
index 75846bc4c..7bfa478ae 100644
--- a/resources/3rdparty/cudd-3.0.0/Makefile.in
+++ b/resources/3rdparty/cudd-3.0.0/Makefile.in
@@ -1,7 +1,7 @@
-# Makefile.in generated by automake 1.15 from Makefile.am.
+# Makefile.in generated by automake 1.15.1 from Makefile.am.
# @configure_input@
-# Copyright (C) 1994-2014 Free Software Foundation, Inc.
+# Copyright (C) 1994-2017 Free Software Foundation, Inc.
# This Makefile.in is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -2850,7 +2850,7 @@ distdir: $(DISTFILES)
! -type d ! -perm -444 -exec $(install_sh) -c -m a+r {} {} \; \
|| chmod -R a+r "$(distdir)"
dist-gzip: distdir
- tardir=$(distdir) && $(am__tar) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).tar.gz
+ tardir=$(distdir) && $(am__tar) | eval GZIP= gzip $(GZIP_ENV) -c >$(distdir).tar.gz
$(am__post_remove_distdir)
dist-bzip2: distdir
@@ -2876,7 +2876,7 @@ dist-shar: distdir
@echo WARNING: "Support for shar distribution archives is" \
"deprecated." >&2
@echo WARNING: "It will be removed altogether in Automake 2.0" >&2
- shar $(distdir) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).shar.gz
+ shar $(distdir) | eval GZIP= gzip $(GZIP_ENV) -c >$(distdir).shar.gz
$(am__post_remove_distdir)
dist-zip: distdir
@@ -2894,7 +2894,7 @@ dist dist-all:
distcheck: dist
case '$(DIST_ARCHIVES)' in \
*.tar.gz*) \
- GZIP=$(GZIP_ENV) gzip -dc $(distdir).tar.gz | $(am__untar) ;;\
+ eval GZIP= gzip $(GZIP_ENV) -dc $(distdir).tar.gz | $(am__untar) ;;\
*.tar.bz2*) \
bzip2 -dc $(distdir).tar.bz2 | $(am__untar) ;;\
*.tar.lz*) \
@@ -2904,7 +2904,7 @@ distcheck: dist
*.tar.Z*) \
uncompress -c $(distdir).tar.Z | $(am__untar) ;;\
*.shar.gz*) \
- GZIP=$(GZIP_ENV) gzip -dc $(distdir).shar.gz | unshar ;;\
+ eval GZIP= gzip $(GZIP_ENV) -dc $(distdir).shar.gz | unshar ;;\
*.zip*) \
unzip $(distdir).zip ;;\
esac
diff --git a/resources/3rdparty/cudd-3.0.0/aclocal.m4 b/resources/3rdparty/cudd-3.0.0/aclocal.m4
index 0de6688a7..b1d04ee86 100644
--- a/resources/3rdparty/cudd-3.0.0/aclocal.m4
+++ b/resources/3rdparty/cudd-3.0.0/aclocal.m4
@@ -1,6 +1,6 @@
-# generated automatically by aclocal 1.15 -*- Autoconf -*-
+# generated automatically by aclocal 1.15.1 -*- Autoconf -*-
-# Copyright (C) 1996-2014 Free Software Foundation, Inc.
+# Copyright (C) 1996-2017 Free Software Foundation, Inc.
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -20,7 +20,7 @@ You have another version of autoconf. It may work, but is not guaranteed to.
If you have problems, you may need to regenerate the build system entirely.
To do so, use the procedure documented by the package, typically 'autoreconf'.])])
-# Copyright (C) 2002-2014 Free Software Foundation, Inc.
+# Copyright (C) 2002-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -35,7 +35,7 @@ AC_DEFUN([AM_AUTOMAKE_VERSION],
[am__api_version='1.15'
dnl Some users find AM_AUTOMAKE_VERSION and mistake it for a way to
dnl require some minimum version. Point them to the right macro.
-m4_if([$1], [1.15], [],
+m4_if([$1], [1.15.1], [],
[AC_FATAL([Do not call $0, use AM_INIT_AUTOMAKE([$1]).])])dnl
])
@@ -51,12 +51,12 @@ m4_define([_AM_AUTOCONF_VERSION], [])
# Call AM_AUTOMAKE_VERSION and AM_AUTOMAKE_VERSION so they can be traced.
# This function is AC_REQUIREd by AM_INIT_AUTOMAKE.
AC_DEFUN([AM_SET_CURRENT_AUTOMAKE_VERSION],
-[AM_AUTOMAKE_VERSION([1.15])dnl
+[AM_AUTOMAKE_VERSION([1.15.1])dnl
m4_ifndef([AC_AUTOCONF_VERSION],
[m4_copy([m4_PACKAGE_VERSION], [AC_AUTOCONF_VERSION])])dnl
_AM_AUTOCONF_VERSION(m4_defn([AC_AUTOCONF_VERSION]))])
-# Copyright (C) 2011-2014 Free Software Foundation, Inc.
+# Copyright (C) 2011-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -118,7 +118,7 @@ AC_SUBST([AR])dnl
# AM_AUX_DIR_EXPAND -*- Autoconf -*-
-# Copyright (C) 2001-2014 Free Software Foundation, Inc.
+# Copyright (C) 2001-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -170,7 +170,7 @@ am_aux_dir=`cd "$ac_aux_dir" && pwd`
# AM_COND_IF -*- Autoconf -*-
-# Copyright (C) 2008-2014 Free Software Foundation, Inc.
+# Copyright (C) 2008-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -207,7 +207,7 @@ fi[]dnl
# AM_CONDITIONAL -*- Autoconf -*-
-# Copyright (C) 1997-2014 Free Software Foundation, Inc.
+# Copyright (C) 1997-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -238,7 +238,7 @@ AC_CONFIG_COMMANDS_PRE(
Usually this means the macro was only invoked conditionally.]])
fi])])
-# Copyright (C) 1999-2014 Free Software Foundation, Inc.
+# Copyright (C) 1999-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -429,7 +429,7 @@ _AM_SUBST_NOTMAKE([am__nodep])dnl
# Generate code to set up dependency tracking. -*- Autoconf -*-
-# Copyright (C) 1999-2014 Free Software Foundation, Inc.
+# Copyright (C) 1999-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -505,7 +505,7 @@ AC_DEFUN([AM_OUTPUT_DEPENDENCY_COMMANDS],
# Do all the work for Automake. -*- Autoconf -*-
-# Copyright (C) 1996-2014 Free Software Foundation, Inc.
+# Copyright (C) 1996-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -702,7 +702,7 @@ for _am_header in $config_headers :; do
done
echo "timestamp for $_am_arg" >`AS_DIRNAME(["$_am_arg"])`/stamp-h[]$_am_stamp_count])
-# Copyright (C) 2001-2014 Free Software Foundation, Inc.
+# Copyright (C) 2001-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -723,7 +723,7 @@ if test x"${install_sh+set}" != xset; then
fi
AC_SUBST([install_sh])])
-# Copyright (C) 2003-2014 Free Software Foundation, Inc.
+# Copyright (C) 2003-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -744,7 +744,7 @@ AC_SUBST([am__leading_dot])])
# Check to see how 'make' treats includes. -*- Autoconf -*-
-# Copyright (C) 2001-2014 Free Software Foundation, Inc.
+# Copyright (C) 2001-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -794,7 +794,7 @@ rm -f confinc confmf
# Fake the existence of programs that GNU maintainers use. -*- Autoconf -*-
-# Copyright (C) 1997-2014 Free Software Foundation, Inc.
+# Copyright (C) 1997-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -833,7 +833,7 @@ fi
# Helper functions for option handling. -*- Autoconf -*-
-# Copyright (C) 2001-2014 Free Software Foundation, Inc.
+# Copyright (C) 2001-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -862,7 +862,7 @@ AC_DEFUN([_AM_SET_OPTIONS],
AC_DEFUN([_AM_IF_OPTION],
[m4_ifset(_AM_MANGLE_OPTION([$1]), [$2], [$3])])
-# Copyright (C) 1999-2014 Free Software Foundation, Inc.
+# Copyright (C) 1999-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -909,7 +909,7 @@ AC_LANG_POP([C])])
# For backward compatibility.
AC_DEFUN_ONCE([AM_PROG_CC_C_O], [AC_REQUIRE([AC_PROG_CC])])
-# Copyright (C) 2001-2014 Free Software Foundation, Inc.
+# Copyright (C) 2001-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -928,7 +928,7 @@ AC_DEFUN([AM_RUN_LOG],
# Check to make sure that the build environment is sane. -*- Autoconf -*-
-# Copyright (C) 1996-2014 Free Software Foundation, Inc.
+# Copyright (C) 1996-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -1009,7 +1009,7 @@ AC_CONFIG_COMMANDS_PRE(
rm -f conftest.file
])
-# Copyright (C) 2009-2014 Free Software Foundation, Inc.
+# Copyright (C) 2009-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -1069,7 +1069,7 @@ AC_SUBST([AM_BACKSLASH])dnl
_AM_SUBST_NOTMAKE([AM_BACKSLASH])dnl
])
-# Copyright (C) 2001-2014 Free Software Foundation, Inc.
+# Copyright (C) 2001-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -1097,7 +1097,7 @@ fi
INSTALL_STRIP_PROGRAM="\$(install_sh) -c -s"
AC_SUBST([INSTALL_STRIP_PROGRAM])])
-# Copyright (C) 2006-2014 Free Software Foundation, Inc.
+# Copyright (C) 2006-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
@@ -1116,7 +1116,7 @@ AC_DEFUN([AM_SUBST_NOTMAKE], [_AM_SUBST_NOTMAKE($@)])
# Check how to create a tarball. -*- Autoconf -*-
-# Copyright (C) 2004-2014 Free Software Foundation, Inc.
+# Copyright (C) 2004-2017 Free Software Foundation, Inc.
#
# This file is free software; the Free Software Foundation
# gives unlimited permission to copy and/or distribute it,
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 6d938735c..3284b353c 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -352,15 +352,27 @@ namespace storm {
return input;
}
+ std::vector<std::shared_ptr<storm::logic::Formula const>> createFormulasToRespect(std::vector<storm::jani::Property> const& properties) {
+ std::vector<std::shared_ptr<storm::logic::Formula const>> result = storm::api::extractFormulasFromProperties(properties);
+
+ for (auto const& property : properties) {
+ if (!property.getFilter().getStatesFormula()->isInitialFormula()) {
+ result.push_back(property.getFilter().getStatesFormula());
+ }
+ }
+
+ return result;
+ }
+
template <storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) {
- return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), storm::api::extractFormulasFromProperties(input.properties));
+ return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties));
}
template <typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
- return storm::api::buildSparseModel<ValueType>(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
+ return storm::api::buildSparseModel<ValueType>(input.model.get(), createFormulasToRespect(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
}
template <typename ValueType>
@@ -416,7 +428,7 @@ namespace storm {
}
STORM_LOG_INFO("Performing bisimulation minimization...");
- return storm::api::performBisimulationMinimization<ValueType>(model, storm::api::extractFormulasFromProperties(input.properties), bisimType);
+ return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType);
}
template <typename ValueType>
@@ -602,9 +614,11 @@ namespace storm {
}
template<typename ValueType>
- void printInitialStatesResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) {
+ void printResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) {
if (result) {
- STORM_PRINT_AND_LOG("Result (initial states): ");
+ std::stringstream ss;
+ ss << "'" << *property.getFilter().getStatesFormula() << "'";
+ STORM_PRINT_AND_LOG("Result (for " << (property.getFilter().getStatesFormula()->isInitialFormula() ? "initial" : ss.str()) << " states): ");
printFilteredResult<ValueType>(result, property.getFilter().getFilterType());
if (watch) {
STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl);
@@ -621,21 +635,22 @@ namespace storm {
};
template<typename ValueType>
- void verifyProperties(std::vector<storm::jani::Property> const& properties, std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback = PostprocessingIdentity()) {
+ void verifyProperties(std::vector<storm::jani::Property> const& properties, std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback = PostprocessingIdentity()) {
for (auto const& property : properties) {
printModelCheckingProperty(property);
storm::utility::Stopwatch watch(true);
- std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula());
+ std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula());
watch.stop();
- printInitialStatesResult<ValueType>(result, property, &watch);
postprocessingCallback(result);
+ printResult<ValueType>(result, property, &watch);
}
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) {
STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
- verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+ verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
return storm::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(input.model.get(), storm::api::createTask<ValueType>(formula, true));
});
}
@@ -644,7 +659,8 @@ namespace storm {
void verifyWithExplorationEngine(SymbolicInput const& input) {
STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
STORM_LOG_THROW((std::is_same<ValueType, double>::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points.");
- verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+ verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states.");
return storm::api::verifyWithExplorationEngine<ValueType>(input.model.get(), storm::api::createTask<ValueType>(formula, true));
});
}
@@ -653,35 +669,60 @@ namespace storm {
void verifyWithSparseEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
verifyProperties<ValueType>(input.properties,
- [&sparseModel] (std::shared_ptr<storm::logic::Formula const> const& formula) {
- std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(formula, true));
- if (result) {
- result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates()));
+ [&sparseModel] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ bool filterForInitialStates = states->isInitialFormula();
+ auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+ std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, task);
+
+ std::unique_ptr<storm::modelchecker::CheckResult> filter;
+ if (filterForInitialStates) {
+ filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(sparseModel->getInitialStates());
+ } else {
+ filter = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(states, false));
}
+ result->filter(filter->asQualitativeCheckResult());
return result;
});
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithHybridEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
- verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+ verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ bool filterForInitialStates = states->isInitialFormula();
+ auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+
auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
- std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(formula, true));
- if (result) {
- result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+ std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, task);
+
+ std::unique_ptr<storm::modelchecker::CheckResult> filter;
+ if (filterForInitialStates) {
+ filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates());
+ } else {
+ filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false));
}
+
+ result->filter(filter->asQualitativeCheckResult());
return result;
});
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyWithDdEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
- verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+ verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ bool filterForInitialStates = states->isInitialFormula();
+ auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+
auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), storm::api::createTask<ValueType>(formula, true));
- if (result) {
- result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+
+ std::unique_ptr<storm::modelchecker::CheckResult> filter;
+ if (filterForInitialStates) {
+ filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates());
+ } else {
+ filter = storm::api::verifyWithDdEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false));
}
+
+ result->filter(filter->asQualitativeCheckResult());
return result;
});
}
diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index 66b5a29fa..b954d4720 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -1,5 +1,6 @@
#include "storm/logic/BoundedUntilFormula.h"
+#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
@@ -80,6 +81,22 @@ namespace storm {
return bound;
}
+ template <>
+ storm::RationalNumber BoundedUntilFormula::getLowerBound() const {
+ checkNoVariablesInBound(this->getLowerBound());
+ storm::RationalNumber bound = this->getLowerBound().evaluateAsRational();
+ STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
+ return bound;
+ }
+
+ template <>
+ storm::RationalNumber BoundedUntilFormula::getUpperBound() const {
+ checkNoVariablesInBound(this->getUpperBound());
+ storm::RationalNumber bound = this->getLowerBound().evaluateAsRational();
+ STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
+ return bound;
+ }
+
template <>
uint64_t BoundedUntilFormula::getLowerBound() const {
checkNoVariablesInBound(this->getLowerBound());
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index 9038a2307..3f871908e 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -175,6 +175,10 @@ namespace storm {
return std::shared_ptr<Formula const>(new BooleanLiteralFormula(true));
}
+ bool Formula::isInitialFormula() const {
+ return this->isAtomicLabelFormula() && this->asAtomicLabelFormula().getLabel() == "init";
+ }
+
PathFormula& Formula::asPathFormula() {
return dynamic_cast<PathFormula&>(*this);
}
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 2ad5e9477..a76dd0ef7 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -93,10 +93,12 @@ namespace storm {
bool isInFragment(FragmentSpecification const& fragment) const;
FormulaInformation info() const;
-
+
virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0;
static std::shared_ptr<Formula const> getTrueFormula();
+
+ bool isInitialFormula() const;
PathFormula& asPathFormula();
PathFormula const& asPathFormula() const;
diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h
index 2488baaaf..7200cc89d 100644
--- a/src/storm/logic/TimeBoundType.h
+++ b/src/storm/logic/TimeBoundType.h
@@ -36,6 +36,11 @@ namespace storm {
bool isRewardBound() const {
return type == TimeBoundType::Reward;
}
+
+ std::string const& getRewardName() const {
+ assert(isRewardBound());
+ return rewardName;
+ }
};
diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp
index bdcf68c8f..9155057d3 100644
--- a/src/storm/modelchecker/results/CheckResult.cpp
+++ b/src/storm/modelchecker/results/CheckResult.cpp
@@ -113,6 +113,15 @@ namespace storm {
return dynamic_cast<QualitativeCheckResult const&>(*this);
}
+ template<typename ValueType>
+ QuantitativeCheckResult<ValueType>& CheckResult::asQuantitativeCheckResult() {
+ return static_cast<QuantitativeCheckResult<ValueType> &>(*this);
+ }
+
+ template<typename ValueType>
+ QuantitativeCheckResult<ValueType> const& CheckResult::asQuantitativeCheckResult() const {
+ return static_cast<QuantitativeCheckResult<ValueType> const&>(*this);
+ }
template <storm::dd::DdType Type>
SymbolicQualitativeCheckResult<Type>& CheckResult::asSymbolicQualitativeCheckResult() {
@@ -155,6 +164,9 @@ namespace storm {
}
// Explicitly instantiate the template functions.
+ template QuantitativeCheckResult<double>& CheckResult::asQuantitativeCheckResult();
+ template QuantitativeCheckResult<double> const& CheckResult::asQuantitativeCheckResult() const;
+
template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
template ExplicitParetoCurveCheckResult<double>& CheckResult::asExplicitParetoCurveCheckResult();
@@ -184,9 +196,15 @@ namespace storm {
#ifdef STORM_HAVE_CARL
+ template QuantitativeCheckResult<storm::RationalNumber>& CheckResult::asQuantitativeCheckResult();
+ template QuantitativeCheckResult<storm::RationalNumber> const& CheckResult::asQuantitativeCheckResult() const;
+
template ExplicitQuantitativeCheckResult<storm::RationalNumber>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<storm::RationalNumber> const& CheckResult::asExplicitQuantitativeCheckResult() const;
+ template QuantitativeCheckResult<storm::RationalFunction>& CheckResult::asQuantitativeCheckResult();
+ template QuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asQuantitativeCheckResult() const;
+
template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;
diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h
index 2cff249c9..43954a220 100644
--- a/src/storm/modelchecker/results/CheckResult.h
+++ b/src/storm/modelchecker/results/CheckResult.h
@@ -66,14 +66,10 @@ namespace storm {
QualitativeCheckResult const& asQualitativeCheckResult() const;
template<typename ValueType>
- QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult() {
- return static_cast<QuantitativeCheckResult<ValueType> &>(*this);
- }
+ QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult();
+
template<typename ValueType>
- QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const {
- return static_cast<QuantitativeCheckResult<ValueType> const&>(*this);
- }
-
+ QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const;
ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const;
diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp
index 45fa27c16..32148b3c3 100644
--- a/src/storm/parser/FormulaParserGrammar.cpp
+++ b/src/storm/parser/FormulaParserGrammar.cpp
@@ -131,7 +131,7 @@ namespace storm {
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses"
- filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > -(qi::lit(",") > qi::lit("\"init\"") > qi::lit(")")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterType, phoenix::ref(*this), qi::_1, qi::_2)];
+ filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)];
filterProperty.name("filter property");
#pragma clang diagnostic pop
@@ -347,8 +347,8 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
}
- storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula) {
- storm::jani::FilterExpression filterExpression(formula, filterType);
+ storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+ storm::jani::FilterExpression filterExpression(formula, filterType, states);
++propertyCount;
if (propertyName) {
@@ -358,7 +358,7 @@ namespace storm {
}
}
- storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterType(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula) {
+ storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula) {
++propertyCount;
if (propertyName) {
return storm::jani::Property(propertyName.get(), formula);
diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h
index 31f766789..d8039bade 100644
--- a/src/storm/parser/FormulaParserGrammar.h
+++ b/src/storm/parser/FormulaParserGrammar.h
@@ -223,8 +223,8 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
std::shared_ptr<storm::logic::Formula const> createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
- storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula);
- storm::jani::Property createPropertyWithDefaultFilterType(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
+ storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states);
+ storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp
index e46d2ee50..73c6d0dec 100644
--- a/src/storm/storage/jani/Property.cpp
+++ b/src/storm/storage/jani/Property.cpp
@@ -5,19 +5,17 @@ namespace storm {
std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) {
- return os << "Obtain " << toString(fe.getFilterType()) << " of the 'initial'-states with values described by '" << *fe.getFormula() << "'";
+ return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'";
}
Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment)
- : name(name), comment(comment), filterExpression(FilterExpression(formula))
- {
-
+ : name(name), comment(comment), filterExpression(FilterExpression(formula)) {
+ // Intentionally left empty.
}
Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment)
- : name(name), comment(comment), filterExpression(fe)
- {
-
+ : name(name), comment(comment), filterExpression(fe) {
+ // Intentionally left empty.
}
std::string const& Property::getName() const {
@@ -48,6 +46,5 @@ namespace storm {
return os << "(" << p.getName() << ") : " << p.getFilter();
}
-
}
}
diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h
index 52db07fef..74aceab5c 100644
--- a/src/storm/storage/jani/Property.h
+++ b/src/storm/storage/jani/Property.h
@@ -2,6 +2,10 @@
#include "storm/modelchecker/results/FilterType.h"
#include "storm/logic/Formulas.h"
+#include "storm/logic/FragmentSpecification.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace jani {
@@ -30,28 +34,35 @@ namespace storm {
public:
FilterExpression() = default;
- explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {}
+ explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES, std::shared_ptr<storm::logic::Formula const> const& statesFormula = std::make_shared<storm::logic::AtomicLabelFormula>("init")) : formula(formula), ft(ft), statesFormula(statesFormula) {
+ STORM_LOG_THROW(statesFormula->isInFragment(storm::logic::propositional()), storm::exceptions::InvalidArgumentException, "Can only filter by propositional formula.");
+ }
std::shared_ptr<storm::logic::Formula const> const& getFormula() const {
return formula;
}
+ std::shared_ptr<storm::logic::Formula const> const& getStatesFormula() const {
+ return statesFormula;
+ }
+
storm::modelchecker::FilterType getFilterType() const {
return ft;
}
FilterExpression substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
- return FilterExpression(formula->substitute(substitution), ft);
+ return FilterExpression(formula->substitute(substitution), ft, statesFormula->substitute(substitution));
}
FilterExpression substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const {
- return FilterExpression(formula->substitute(labelSubstitution), ft);
+ return FilterExpression(formula->substitute(labelSubstitution), ft, statesFormula->substitute(labelSubstitution));
}
private:
// For now, we assume that the states are always the initial states.
std::shared_ptr<storm::logic::Formula const> formula;
storm::modelchecker::FilterType ft;
+ std::shared_ptr<storm::logic::Formula const> statesFormula;
};