sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge remote-tracking branch 'origin/master' into deterministicScheds

main
Tim Quatmann 6 years ago
parent
b190fe6e8f 9c52d0d2ab
commit
5683ffd7bd
16 changed files with 79 additions and 31 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 32
      resources/3rdparty/CMakeLists.txt
  2. 15
      src/storm-gspn/adapters/XercesAdapter.h
  3. 7
      src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp
  4. 4
      src/storm-pomdp/storage/PomdpMemory.cpp
  5. 7
      src/storm/analysis/GraphConditions.cpp
  6. 2
      src/storm/builder/DdJaniModelBuilder.cpp
  7. 4
      src/storm/logic/Bound.h
  8. 5
      src/storm/logic/ComparisonType.h
  9. 3
      src/storm/modelchecker/results/FilterType.cpp
  10. 4
      src/storm/solver/LinearEquationSolverRequirements.cpp
  11. 4
      src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp
  12. 2
      src/storm/solver/Multiplier.cpp
  13. 2
      src/storm/storage/dd/bisimulation/SignatureComputer.cpp
  14. 10
      src/storm/storage/jani/JSONExporter.cpp
  15. 5
      src/storm/utility/builder.cpp
  16. 4
      src/storm/utility/shortestPaths.cpp

32
resources/3rdparty/CMakeLists.txt
View File

@ -562,9 +562,35 @@ if (STORM_USE_INTELTBB)
message(STATUS "Storm - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.")
message(STATUS "Storm - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.")
set(STORM_HAVE_INTELTBB ON)
link_directories(${TBB_LIBRARY_DIRS})
include_directories(${TBB_INCLUDE_DIRS})
list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc)
# Under Linux libtbb.so contains a linker script to libtbb.so.2 instead of a symlink.
# This breaks CMake.
# As a workaround we manually try to add the necessary suffix ".2" to the so file and hope for the best.
if (LINUX)
# Check if the library is a linker script which only links to the correct library
# Read first bytes of file
file(READ "${TBB_LIBRARY}" TMPTXT LIMIT 128)
# Check if file starts with "INPUT (libtbb.so.2)"
if("${TMPTXT}" MATCHES "INPUT \\(libtbb\\.so\\.(.*)\\)")
# Manually set library by adding the suffix from the linker script.
# CMAKE_MATCH_1 contains the parsed suffix.
set(TBB_LIB_LINUX "${TBB_LIBRARY}.${CMAKE_MATCH_1}")
set(TBB_MALLOC_LIB_LINUX "${TBB_MALLOC_LIBRARY}.${CMAKE_MATCH_1}")
if (EXISTS "${TBB_LIB_LINUX}")
set(TBB_LIBRARY ${TBB_LIB_LINUX})
message(STATUS "Storm - Using Intel TBB library in manually set path ${TBB_LIBRARY}.")
endif()
if (EXISTS "${TBB_MALLOC_LIB_LINUX}")
set(TBB_MALLOC_LIBRARY ${TBB_MALLOC_LIB_LINUX})
message(STATUS "Storm - Using Intel TBB malloc library in manually set path ${TBB_MALLOC_LIBRARY}.")
endif()
endif()
endif()
add_imported_library(tbb SHARED ${TBB_LIBRARY} ${TBB_INCLUDE_DIRS})
list(APPEND STORM_DEP_TARGETS tbb_SHARED)
add_imported_library(tbb_malloc SHARED ${TBB_MALLOC_LIBRARY} ${TBB_INCLUDE_DIRS})
list(APPEND STORM_DEP_TARGETS tbb_malloc_SHARED)
else(TBB_FOUND)
message(FATAL_ERROR "Storm - TBB was requested, but not found.")
endif(TBB_FOUND)

15
src/storm-gspn/adapters/XercesAdapter.h
View File

@ -10,7 +10,8 @@
#include <xercesc/sax/HandlerBase.hpp>
#include <xercesc/util/PlatformUtils.hpp>
#include "storm/utility/macros.h"
#include "storm/exceptions/IllegalArgumentException.h"
namespace storm {
namespace adapters {
@ -27,16 +28,12 @@ namespace storm {
auto elementNode = (xercesc::DOMElement *) node;
return XMLtoString(elementNode->getTagName());
}
case xercesc::DOMNode::NodeType::TEXT_NODE: {
case xercesc::DOMNode::NodeType::TEXT_NODE:
return XMLtoString(node->getNodeValue());
}
case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: {
case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE:
return XMLtoString(node->getNodeName());
}
default: {
assert(false);
return "";
}
default:
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown DOMNode type");
}
}
}

7
src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp
View File

@ -1,6 +1,7 @@
#include "JaniProgramGraphBuilder.h"
#include "storm/storage/jani/EdgeDestination.h"
#include "storm/exceptions/NotSupportedException.h"
namespace storm {
namespace builder {
@ -23,12 +24,10 @@ namespace storm {
variables.emplace(v.first, janiVar);
automaton.addVariable(*janiVar);
} else {
// Not yet supported.
assert(false);
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unbounded right bound is not supported yet");
}
} else {
// Not yet supported.
assert(false);
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unbounded left bound is not supported yet");
}
} else {
storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first));

4
src/storm-pomdp/storage/PomdpMemory.cpp
View File

@ -2,6 +2,7 @@
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/IllegalArgumentException.h"
namespace storm {
namespace storage {
@ -110,6 +111,7 @@ namespace storm {
case PomdpMemoryPattern::Full:
return buildFullyConnectedMemory(numStates);
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown PomdpMemoryPattern");
}
PomdpMemory PomdpMemoryBuilder::buildTrivialMemory() const {
@ -177,4 +179,4 @@ namespace storm {
return PomdpMemory(transitions, 0);
}
}
}
}

7
src/storm/analysis/GraphConditions.cpp
View File

@ -4,6 +4,7 @@
#include "GraphConditions.h"
#include "storm/utility/constants.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/models/sparse/StandardRewardModel.h"
namespace storm {
@ -44,7 +45,7 @@ namespace storm {
} else if (entry.denominator().constantPart() < 0) {
wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
} else {
assert(false); // Should fail before.
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before.");
}
} else {
wellformedConstraintSet.emplace(entry.denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
@ -111,7 +112,7 @@ namespace storm {
} else if (transition.getValue().denominator().constantPart() < 0) {
wellformedConstraintSet.emplace(transition.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
} else {
assert(false); // Should fail before.
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before.");
}
} else {
wellformedConstraintSet.emplace(transition.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);
@ -147,7 +148,7 @@ namespace storm {
} else if (entry.getValue().denominator().constantPart() < 0) {
wellformedConstraintSet.emplace(entry.getValue().nominator().polynomialWithCoefficient(), storm::CompareRelation::LEQ);
} else {
assert(false); // Should fail before.
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should have failed before.");
}
} else {
wellformedConstraintSet.emplace(entry.getValue().denominator().polynomialWithCoefficient(), storm::CompareRelation::NEQ);

2
src/storm/builder/DdJaniModelBuilder.cpp
View File

@ -733,7 +733,7 @@ namespace storm {
// Intentionally left empty.
}
bool setMarkovian(bool markovian) {
void setMarkovian(bool markovian) {
this->markovian = markovian;
}

4
src/storm/logic/Bound.h
View File

@ -1,10 +1,11 @@
#ifndef STORM_LOGIC_BOUND_H_
#define STORM_LOGIC_BOUND_H_
#include "storm/exceptions/IllegalArgumentException.h"
#include "storm/logic/ComparisonType.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
namespace storm {
namespace logic {
@ -29,6 +30,7 @@ namespace storm {
case ComparisonType::LessEqual:
return compareValue <= thresholdAsValueType;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType");
}
friend std::ostream& operator<<(std::ostream& out, Bound const& bound);

5
src/storm/logic/ComparisonType.h
View File

@ -3,6 +3,9 @@
#include <iostream>
#include "storm/utility/macros.h"
#include "storm/exceptions/IllegalArgumentException.h"
namespace storm {
namespace logic {
enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual };
@ -26,6 +29,7 @@ namespace storm {
case ComparisonType::GreaterEqual:
return ComparisonType::Less;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType");
}
inline ComparisonType invertPreserveStrictness(ComparisonType t) {
@ -39,6 +43,7 @@ namespace storm {
case ComparisonType::GreaterEqual:
return ComparisonType::LessEqual;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType");
}
std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType);

3
src/storm/modelchecker/results/FilterType.cpp
View File

@ -1,5 +1,7 @@
#include "FilterType.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/IllegalArgumentException.h"
namespace storm {
namespace modelchecker {
@ -27,6 +29,7 @@ namespace storm {
case FilterType::VALUES:
return "the values";
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType");
}
}
}

4
src/storm/solver/LinearEquationSolverRequirements.cpp
View File

@ -1,5 +1,8 @@
#include "storm/solver/LinearEquationSolverRequirements.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/IllegalArgumentException.h"
namespace storm {
namespace solver {
@ -36,6 +39,7 @@ namespace storm {
case Element::LowerBounds: return lowerBounds(); break;
case Element::UpperBounds: return upperBounds(); break;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ElementType");
}
void LinearEquationSolverRequirements::clearLowerBounds() {

4
src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp
View File

@ -1,5 +1,8 @@
#include "storm/solver/MinMaxLinearEquationSolverRequirements.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/IllegalArgumentException.h"
namespace storm {
namespace solver {
@ -56,6 +59,7 @@ namespace storm {
case Element::LowerBounds: return lowerBounds(); break;
case Element::UpperBounds: return upperBounds(); break;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ElementType");
}
void MinMaxLinearEquationSolverRequirements::clearUniqueSolution() {

2
src/storm/solver/Multiplier.cpp
View File

@ -12,6 +12,7 @@
#include "storm/solver/NativeMultiplier.h"
#include "storm/solver/GmmxxMultiplier.h"
#include "storm/environment/solver/MultiplierEnvironment.h"
#include "storm/exceptions/IllegalArgumentException.h"
namespace storm {
namespace solver {
@ -79,6 +80,7 @@ namespace storm {
case MultiplierType::Native:
return std::make_unique<NativeMultiplier<ValueType>>(matrix);
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType");
}
template class Multiplier<double>;

2
src/storm/storage/dd/bisimulation/SignatureComputer.cpp
View File

@ -6,6 +6,7 @@
#include "storm/utility/macros.h"
#include "storm/exceptions/OutOfRangeException.h"
#include "storm/exceptions/IllegalArgumentException.h"
namespace storm {
namespace dd {
@ -23,6 +24,7 @@ namespace storm {
case SignatureMode::Eager: return position < 1;
case SignatureMode::Lazy: return position < 2;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown SignatureMode");
}
template<storm::dd::DdType DdType, typename ValueType>

10
src/storm/storage/jani/JSONExporter.cpp
View File

@ -12,6 +12,7 @@
#include "storm/exceptions/InvalidJaniException.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/IllegalArgumentException.h"
#include "storm/storage/expressions/RationalLiteralExpression.h"
#include "storm/storage/expressions/IntegerLiteralExpression.h"
@ -120,9 +121,8 @@ namespace storm {
return ">";
case storm::logic::ComparisonType::GreaterEqual:
return "≥";
default:
assert(false);
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType");
}
modernjson::json numberToJson(storm::RationalNumber rn) {
@ -796,7 +796,7 @@ namespace storm {
typeDescr["kind"] = "array";
typeDescr["base"] = buildTypeDescription(type.getElementType());
} else {
assert(false);
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown expression type.");
}
return typeDescr;
}
@ -1104,10 +1104,8 @@ namespace storm {
return "argmax";
case storm::modelchecker::FilterType::VALUES:
return "values";
default:
assert(false);
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType");
}
modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {

5
src/storm/utility/builder.cpp
View File

@ -7,6 +7,8 @@
#include "storm/models/sparse/Pomdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/exceptions/InvalidModelException.h"
namespace storm {
namespace utility {
namespace builder {
@ -27,6 +29,7 @@ namespace storm {
case storm::models::ModelType::S2pg:
return std::make_shared<storm::models::sparse::StochasticTwoPlayerGame<ValueType, RewardModelType>>(std::move(components));
}
STORM_LOG_THROW(false, storm::exceptions::InvalidModelException, "Unknown model type");
}
template std::shared_ptr<storm::models::sparse::Model<double>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<double>&& components);
@ -35,4 +38,4 @@ namespace storm {
template std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<storm::RationalFunction>&& components);
}
}
}
}

4
src/storm/utility/shortestPaths.cpp
View File

@ -9,6 +9,7 @@
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/shortestPaths.h"
#include "storm/exceptions/UnexpectedException.h"
// FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required!
// (Also, did I document this? I think so, somewhere. I went with k>=1 because
@ -247,8 +248,7 @@ namespace storm {
// there is no such edge
// let's disallow that for now, because I'm not expecting it to happen
assert(false);
return zero<T>();
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Should not happen.");
} else {
// edge must be "virtual edge" to meta-target
assert(isMetaTargetPredecessor(tailNode));

Write Preview
Loading…
Cancel
Save