diff --git a/.travis.yml b/.travis.yml
index c824cddf6..2b5f50657 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -243,6 +243,57 @@ jobs:
after_failure:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
+ ###
+ # Stage: Build (5th run)
+ ###
+
+ # osx
+ - stage: Build (5th run)
+ os: osx
+ compiler: clang
+ env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+ install:
+ - travis/install_osx.sh
+ script:
+ - travis/build.sh BuildLast
+ after_failure:
+ - find build -iname '*err*.log' -type f -print -exec cat {} \;
+ - stage: Build (5th run)
+ os: osx
+ compiler: clang
+ env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+ install:
+ - travis/install_osx.sh
+ script:
+ - travis/build.sh BuildLast
+ after_failure:
+ - find build -iname '*err*.log' -type f -print -exec cat {} \;
+ # ubuntu-16.10
+ - stage: Build (5th run)
+ os: linux
+ compiler: gcc
+ env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+ install:
+ - travis/install_linux.sh
+ script:
+ - travis/build.sh BuildLast
+ before_cache:
+ - docker cp storm:/storm/. .
+ after_failure:
+ - find build -iname '*err*.log' -type f -print -exec cat {} \;
+ - stage: Build (5th run)
+ os: linux
+ compiler: gcc
+ env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+ install:
+ - travis/install_linux.sh
+ script:
+ - travis/build.sh BuildLast
+ before_cache:
+ - docker cp storm:/storm/. .
+ after_failure:
+ - find build -iname '*err*.log' -type f -print -exec cat {} \;
+
###
# Stage: Test all
###
diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
index 09fb51ccf..fb92720d0 100644
--- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp
+++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
@@ -125,8 +125,6 @@ int storm_rational_number_is_zero(storm_rational_number_ptr a) {
std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif
- std::cout << "got ptr for eq check " << a << std::endl;
-
return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0;
}
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 8f23d14ce..a550ee130 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -1088,6 +1088,7 @@ namespace storm {
std::stringstream tmp;
indent(tmp, indentLevel + 1) << "{% for reward in destination_rewards %}choice.addReward({$reward.index}, probability * transientOut.{$reward.variable});" << std::endl;
indent(tmp, indentLevel + 1) << "{% endfor %}" << std::endl;
+ vectorSource << cpptempl::parse(tmp.str(), modelData);
indent(vectorSource, indentLevel) << "}" << std::endl << std::endl;
indent(vectorSource, indentLevel) << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& in, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore, ";
@@ -2309,8 +2310,8 @@ namespace storm {
{% if dontFixDeadlocks %}
if (behaviour.empty() && behaviour.isExpanded() ) {
- std::cout << currentState << std::endl;
- throw storm::exceptions::WrongFormatException("Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled.");
+ std::cout << "found deadlock state: " << currentState << std::endl;
+ throw storm::exceptions::WrongFormatException("Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled.");
}
{% endif %}
diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp
index 00eee1e01..bc5c43ed9 100644
--- a/src/storm/logic/VariableSubstitutionVisitor.cpp
+++ b/src/storm/logic/VariableSubstitutionVisitor.cpp
@@ -43,7 +43,6 @@ namespace storm {
std::vector<storm::logic::TimeBoundReference> tbReferences;
for (unsigned i = 0; i < f.getDimension(); ++i) {
- std::cout << f.hasLowerBound(i) << std::endl;
if (f.hasLowerBound(i)) {
lowerBounds.push_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i).substitute(substitution)));
} else {
@@ -53,7 +52,7 @@ namespace storm {
if (f.hasUpperBound(i)) {
upperBounds.push_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i).substitute(substitution)));
} else {
- lowerBounds.push_back(boost::none);
+ upperBounds.push_back(boost::none);
}
tbReferences.push_back(f.getTimeBoundReference(i));
}
diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h
index 4440f1ba3..828f85215 100644
--- a/src/storm/modelchecker/CheckTask.h
+++ b/src/storm/modelchecker/CheckTask.h
@@ -52,6 +52,7 @@ namespace storm {
template<typename NewFormulaType>
CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
CheckTask<NewFormulaType, ValueType> result(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint);
+ result.updateOperatorInformation();
return result;
}
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index a87ea5888..387423066 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -492,6 +492,11 @@ namespace storm {
}
}
+ // If there are no variables, there is no restriction on the initial states.
+ if (!result.isInitialized()) {
+ result = manager->boolean(true);
+ }
+
return result;
}
}
diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp
index 13065000a..c341cdc22 100644
--- a/src/storm/utility/graph.cpp
+++ b/src/storm/utility/graph.cpp
@@ -165,7 +165,7 @@ namespace storm {
}
candidateStates = storm::utility::graph::getReachableStates(transitionMatrix, choiceTargets, candidateStates, storm::storage::BitVector(candidateStates.size(), false));
- // At this point we know that every candidate state can reach a choice at least once without leaving the set of candidate states.
+ // At this point we know that every candidate state can reach a state with a choice without leaving the set of candidate states.
// We now compute the states that can reach a choice at least twice, three times, four times, ... until a fixpoint is reached.
while (!candidateStates.empty()) {
// Update the states with a choice that stays within the set of candidates
@@ -193,11 +193,12 @@ namespace storm {
// Update the candidates
storm::storage::BitVector newCandidates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, statesWithChoice);
- // Check if conferged
+ // Check if converged
if (newCandidates == candidateStates) {
assert(!candidateStates.empty());
return true;
}
+ candidateStates = std::move(newCandidates);
}
return false;
}
diff --git a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
index b78eead1b..ad9699e46 100644
--- a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
@@ -16,23 +16,19 @@
#include "storm/api/storm.h"
-/* Rationals for MAs not supported at this point
TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma";
std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto
- // formulasAsString += "; \n multi(..)";
// programm, model, formula
storm::prism::Program program = storm::api::parseProgram(programFile);
program.checkValidity();
- std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(parseFormulasForProgram(formulasAsString, program));
+ std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
storm::generator::NextStateGeneratorOptions options(formulas);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> ma = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build()->as<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>();
- storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> checker(*ma);
-
- std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[0], true));
+ std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
storm::RationalNumber p1 = storm::utility::convertNumber<storm::RationalNumber>(11.0); p1 /= storm::utility::convertNumber<storm::RationalNumber>(6.0);
@@ -45,7 +41,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) {
EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
-}*/
+}
TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) {
diff --git a/travis/build-helper.sh b/travis/build-helper.sh
index c6f2dff60..8d73c87e7 100755
--- a/travis/build-helper.sh
+++ b/travis/build-helper.sh
@@ -13,7 +13,7 @@ travis_fold() {
# Helper for distinguishing between different runs
run() {
case "$1" in
- Build1 | Build2 | Build3 | Build4)
+ Build*)
if [[ "$1" == "Build1" ]]
then
# CMake
@@ -38,7 +38,7 @@ run() {
make -j$N_JOBS
travis_fold end make
# Set skip-file
- if [[ "$1" != "Build4" ]]
+ if [[ "$1" != "BuildLast" ]]
then
touch skip.txt
else
diff --git a/travis/build.sh b/travis/build.sh
index 0b7900e70..668e4f18e 100755
--- a/travis/build.sh
+++ b/travis/build.sh
@@ -13,7 +13,7 @@ EXITCODE=42
if [ -f build/skip.txt ]
then
# Remove flag s.t. tests will be executed
- if [[ "$1" == "Build4" ]]
+ if [[ "$1" == "BuildLast" ]]
then
rm build/skip.txt
fi
@@ -63,7 +63,7 @@ osx)
exit 1
esac
-if [[ $EXITCODE == 124 ]] && [[ "$1" == Build* ]] && [[ "$1" != "Build4" ]]
+if [[ $EXITCODE == 124 ]] && [[ "$1" == Build* ]] && [[ "$1" != "BuildLast" ]]
then
exit 0
else
diff --git a/travis/generate_travis.py b/travis/generate_travis.py
index c47afac0c..14e058a85 100644
--- a/travis/generate_travis.py
+++ b/travis/generate_travis.py
@@ -24,6 +24,7 @@ stages = [
("Build (2nd run)", "Build2"),
("Build (3rd run)", "Build3"),
("Build (4th run)", "Build4"),
+ ("Build (5th run)", "BuildLast"),
("Test all", "TestAll"),
]