Browse Source

Merge branch 'master' into pomdp-building

main
Sebastian Junges 5 years ago
parent
commit
fe21001eb3
  1. 1
      CHANGELOG.md
  2. 2
      CMakeLists.txt
  3. 155
      resources/examples/testfiles/ma/chain_elimination1.drn
  4. 34
      resources/examples/testfiles/ma/chain_elimination2.drn
  5. 8
      src/storm-cli-utilities/model-handling.h
  6. 2
      src/storm-dft/settings/DftSettings.cpp
  7. 4
      src/storm-pars/settings/ParsSettings.cpp
  8. 32
      src/storm-parsers/parser/DirectEncodingParser.cpp
  9. 9
      src/storm-parsers/parser/DirectEncodingParser.h
  10. 4
      src/storm/api/builder.h
  11. 27
      src/storm/models/sparse/ItemLabeling.cpp
  12. 17
      src/storm/models/sparse/ItemLabeling.h
  13. 4
      src/storm/models/sparse/MarkovAutomaton.cpp
  14. 4
      src/storm/models/sparse/StateLabeling.cpp
  15. 8
      src/storm/models/sparse/StateLabeling.h
  16. 2
      src/storm/settings/SettingsManager.cpp
  17. 43
      src/storm/settings/modules/HintSettings.cpp
  18. 40
      src/storm/settings/modules/HintSettings.h
  19. 2
      src/storm/solver/stateelimination/NondeterministicModelStateEliminator.h
  20. 5
      src/storm/storage/BitVector.cpp
  21. 178
      src/storm/storage/BitVector.h
  22. 8
      src/storm/storage/jani/Model.cpp
  23. 10
      src/storm/storage/jani/Model.h
  24. 14
      src/storm/storage/jani/VariableSet.cpp
  25. 20
      src/storm/storage/jani/VariableSet.h
  26. 20
      src/storm/storage/jani/traverser/InformationCollector.cpp
  27. 20
      src/storm/storage/jani/traverser/InformationCollector.h
  28. 357
      src/storm/transformer/NonMarkovianChainTransformer.cpp
  29. 7
      src/storm/transformer/NonMarkovianChainTransformer.h
  30. 4
      src/storm/utility/DirectEncodingExporter.cpp
  31. 37
      src/test/storm/model/StateLabelingTest.cpp
  32. 249
      src/test/storm/transformer/NonMarkovianChainTransformerTest.cpp

1
CHANGELOG.md

@ -8,6 +8,7 @@ Version 1.4.x
-------------
## Version 1.4.2 (under development)
- DRN: support import of choice labelling
- `storm-pomdp`: Only accept POMDPs that are canonical
- `storm-pomdp`: Prism language extended with observable expressions
- `storm-pomdp`: Various fixes that prevented usage.

2
CMakeLists.txt

@ -493,7 +493,7 @@ include(CTest)
# Compiles all tests
add_custom_target(tests)
# Compiles and runs all tests
add_custom_target(check COMMAND ${CMAKE_CTEST_COMMAND})
add_custom_target(check COMMAND ${CMAKE_CTEST_COMMAND} --output-on-failure)
set(CMAKE_CTEST_COMMAND_VERBOSE ${CMAKE_CTEST_COMMAND} -V)
add_custom_target(check-verbose COMMAND ${CMAKE_CTEST_COMMAND_VERBOSE})
add_dependencies(check tests)

155
resources/examples/testfiles/ma/chain_elimination1.drn

@ -0,0 +1,155 @@
// Exported by storm
// Original model type: Markov Automaton
@type: Markov Automaton
@parameters
@reward_models
@nr_states
43
@model
state 0 !0 init
action 0
1 : 1
state 1 !0.0003
action 0
2 : 0.3333333333
3 : 0.3333333333
4 : 0.3333333333
state 2 !0
action 0
5 : 1
state 3 !0
action 0
6 : 1
state 4 !0
action 0
7 : 1
state 5 !0
action 0
8 : 1
state 6 !0
action 0
9 : 1
state 7 !0
action 0
10 : 1
state 8 !0
action 0
12 : 1
state 9 !0
action 0
14 : 1
state 10 !0.1002 Fail
action 0
11 : 0.000998003992
13 : 0.000998003992
15 : 0.998003992
state 11 !0 Fail
action 0
18 : 1
state 12 !0.1002 Fail
action 0
16 : 0.000998003992
19 : 0.000998003992
20 : 0.998003992
state 13 !0 Fail
action 0
21 : 1
state 14 !0.1002 Fail
action 0
17 : 0.000998003992
22 : 0.000998003992
23 : 0.998003992
state 15 !0 Fail
action 0
24 : 1
state 16 !0 Fail
action 0
25 : 1
state 17 !0 Fail
action 0
25 : 1
state 18 !0 Fail
action 0
26 : 1
state 19 !0 Fail
action 0
26 : 1
state 20 !0 Fail
action 0
27 : 1
state 21 !0 Fail
action 0
28 : 1
state 22 !0 Fail
action 0
28 : 1
state 23 !0 Fail
action 0
27 : 1
state 24 !0 Fail
action 0
1 : 1
state 25 !0.2001 Fail
action 0
31 : 0.0004997501249
32 : 0.4997501249
33 : 0.4997501249
state 26 !0.2001 Fail
action 0
29 : 0.0004997501249
34 : 0.4997501249
35 : 0.4997501249
state 27 !0 Fail
action 0
24 : 1
state 28 !0.2001 Fail
action 0
30 : 0.0004997501249
36 : 0.4997501249
37 : 0.4997501249
state 29 !0 Fail
action 0
38 : 1
state 30 !0 Fail
action 0
38 : 1
state 31 !0 Fail
action 0
38 : 1
state 32 !0 Fail
action 0
14 : 1
state 33 !0 Fail
action 0
12 : 1
state 34 !0 Fail
action 0
12 : 1
state 35 !0 Fail
action 0
39 : 1
state 36 !0 Fail
action 0
14 : 1
state 37 !0 Fail
action 0
39 : 1
state 38 !0.3 Fail
action 0
40 : 0.3333333333
41 : 0.3333333333
42 : 0.3333333333
state 39 !0 Fail
action 0
10 : 1
state 40 !0 Fail
action 0
25 : 1
state 41 !0 Fail
action 0
28 : 1
state 42 !0 Fail
action 0
26 : 1

34
resources/examples/testfiles/ma/chain_elimination2.drn

@ -0,0 +1,34 @@
// Exported by storm
// Original model type: Markov Automaton
@type: Markov Automaton
@parameters
@reward_models
@nr_states
10
@model
state 0 !0.1 init
1 : 1
state 1 !0
2 : 1
state 2 !0
3 : 1
state 3 !0
4 : 0.1
5 : 0.9
state 4 !0.2 Fail
5 : 0.5
6 : 0.5
state 5 !0.1
0 : 1
state 6 !0.2
0 : 0.5
7 : 0.5
state 7 !0.2 Fail
6 : 0.5
8 : 0.5
state 8 !0 Fail
9 : 1
state 9 !0 Fail
3 : 1

8
src/storm-cli-utilities/model-handling.h

@ -292,12 +292,14 @@ namespace storm {
}
template <typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings) {
std::shared_ptr<storm::models::ModelBase> buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings, storm::settings::modules::BuildSettings const& buildSettings) {
std::shared_ptr<storm::models::ModelBase> result;
if (ioSettings.isExplicitSet()) {
result = storm::api::buildExplicitModel<ValueType>(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional<std::string>(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional<std::string>(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional<std::string>(ioSettings.getChoiceLabelingFilename()) : boost::none);
} else if (ioSettings.isExplicitDRNSet()) {
result = storm::api::buildExplicitDRNModel<ValueType>(ioSettings.getExplicitDRNFilename());
storm::parser::DirectEncodingParserOptions options;
options.buildChoiceLabeling = buildSettings.isBuildChoiceLabelsSet();
result = storm::api::buildExplicitDRNModel<ValueType>(ioSettings.getExplicitDRNFilename(), options);
} else {
STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type.");
result = storm::api::buildExplicitIMCAModel<ValueType>(ioSettings.getExplicitIMCAFilename());
@ -320,7 +322,7 @@ namespace storm {
}
} else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {
STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input.");
result = buildModelExplicit<ValueType>(ioSettings);
result = buildModelExplicit<ValueType>(ioSettings, buildSettings);
}
modelBuildingWatch.stop();

2
src/storm-dft/settings/DftSettings.cpp

@ -24,6 +24,7 @@
#include "storm-gspn/settings/modules/GSPNSettings.h"
#include "storm-gspn/settings/modules/GSPNExportSettings.h"
#include "storm/settings/modules/TransformationSettings.h"
#include "storm/settings/modules/HintSettings.h"
namespace storm {
@ -39,6 +40,7 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::IOSettings>();
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::TransformationSettings>();
storm::settings::addModule<storm::settings::modules::HintSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();

4
src/storm-pars/settings/ParsSettings.cpp

@ -26,6 +26,8 @@
#include "storm/settings/modules/JitBuilderSettings.h"
#include "storm/settings/modules/MultiplierSettings.h"
#include "storm/settings/modules/TransformationSettings.h"
#include "storm/settings/modules/HintSettings.h"
namespace storm {
@ -57,6 +59,8 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
storm::settings::addModule<storm::settings::modules::TransformationSettings>();
storm::settings::addModule<storm::settings::modules::HintSettings>();
}
}

32
src/storm-parsers/parser/DirectEncodingParser.cpp

@ -28,7 +28,7 @@ namespace storm {
namespace parser {
template<typename ValueType, typename RewardModelType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::parseModel(std::string const& filename) {
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::parseModel(std::string const& filename, DirectEncodingParserOptions const& options) {
// Load file
STORM_LOG_INFO("Reading from file " << filename);
@ -42,6 +42,7 @@ namespace storm {
bool sawParameters = false;
std::unordered_map<std::string, ValueType> placeholders;
size_t nrStates = 0;
size_t nrChoices = 0;
storm::models::ModelType type;
std::vector<std::string> rewardModelNames;
std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents;
@ -102,14 +103,19 @@ namespace storm {
STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice");
std::getline(file, line);
nrStates = parseNumber<size_t>(line);
} else if (line == "@nr_choices") {
STORM_LOG_THROW(nrChoices == 0, storm::exceptions::WrongFormatException, "Number of actions declared twice");
std::getline(file, line);
nrChoices = parseNumber<size_t>(line);
} else if (line == "@model") {
// Parse rest of the model
STORM_LOG_THROW(sawType, storm::exceptions::WrongFormatException, "Type has to be declared before model.");
STORM_LOG_THROW(sawParameters, storm::exceptions::WrongFormatException, "Parameters have to be declared before model.");
STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "No. of states has to be declared before model.");
STORM_LOG_THROW(!options.buildChoiceLabeling || nrChoices != 0, storm::exceptions::WrongFormatException, "No. of actions (@nr_choices) has to be declared before model.");
STORM_LOG_WARN_COND(nrChoices != 0, "No. of actions has to be declared. We may continue now, but future versions might not support this.");
// Construct model components
modelComponents = parseStates(file, type, nrStates, placeholders, valueParser, rewardModelNames);
modelComponents = parseStates(file, type, nrStates, nrChoices, placeholders, valueParser, rewardModelNames, options);
break;
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse line '" << line << "'.");
@ -124,9 +130,9 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>
DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize,
DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, size_t nrChoices,
std::unordered_map<std::string, ValueType> const& placeholders, ValueParser<ValueType> const& valueParser,
std::vector<std::string> const& rewardModelNames) {
std::vector<std::string> const& rewardModelNames, DirectEncodingParserOptions const& options) {
// Initialize
auto modelComponents = std::make_shared<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>();
bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton || type == storm::models::ModelType::Pomdp);
@ -135,6 +141,9 @@ namespace storm {
modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize);
modelComponents->observabilityClasses = std::vector<uint32_t>();
modelComponents->observabilityClasses->resize(stateSize);
if (options.buildChoiceLabeling) {
modelComponents->choiceLabeling = storm::models::sparse::ChoiceLabeling(nrChoices);
}
std::vector<std::vector<ValueType>> stateRewards;
std::vector<std::vector<ValueType>> actionRewards;
if (continuousTime) {
@ -296,8 +305,16 @@ namespace storm {
} else {
line = "";
}
size_t parsedId = parseNumber<size_t>(curString);
STORM_LOG_ASSERT(row == firstRowOfState + parsedId, "Action ids do not correspond.");
// curString contains action name.
if (options.buildChoiceLabeling) {
if (curString != "__NOLABEL__") {
if (!modelComponents->choiceLabeling.get().containsLabel(curString)) {
modelComponents->choiceLabeling.get().addLabel(curString);
}
modelComponents->choiceLabeling.get().addLabelToChoice(curString, row);
}
}
// Check for rewards
if (boost::starts_with(line, "[")) {
// Rewards found
@ -323,7 +340,6 @@ namespace storm {
}
line = line.substr(posEndReward + 1);
}
// TODO import choice labeling when the export works
} else {
// New transition

9
src/storm-parsers/parser/DirectEncodingParser.h

@ -9,6 +9,9 @@
namespace storm {
namespace parser {
struct DirectEncodingParserOptions {
bool buildChoiceLabeling = false;
};
/*!
* Parser for models in the DRN format with explicit encoding.
*/
@ -23,7 +26,7 @@ namespace storm {
*
* @return A sparse model
*/
static std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> parseModel(std::string const& file);
static std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> parseModel(std::string const& fil, DirectEncodingParserOptions const& options = DirectEncodingParserOptions());
private:
@ -40,8 +43,8 @@ namespace storm {
* @return Transition matrix.
*/
static std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>
parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, std::unordered_map<std::string, ValueType> const& placeholders,
ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames);
parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, size_t nrChoices, std::unordered_map<std::string, ValueType> const& placeholders,
ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames, DirectEncodingParserOptions const& options);
/*!
* Parse value from string while using placeholders.

4
src/storm/api/builder.h

@ -144,8 +144,8 @@ namespace storm {
}
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitDRNModel(std::string const& drnFile) {
return storm::parser::DirectEncodingParser<ValueType>::parseModel(drnFile);
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitDRNModel(std::string const& drnFile, storm::parser::DirectEncodingParserOptions const& options = storm::parser::DirectEncodingParserOptions()) {
return storm::parser::DirectEncodingParser<ValueType>::parseModel(drnFile, options);
}
template<typename ValueType>

27
src/storm/models/sparse/ItemLabeling.cpp

@ -64,6 +64,25 @@ namespace storm {
addLabel(label, storage::BitVector(itemCount));
}
void ItemLabeling::removeLabel(std::string const& label) {
auto labelIt = nameToLabelingIndexMap.find(label);
STORM_LOG_THROW(labelIt != nameToLabelingIndexMap.end(), storm::exceptions::InvalidArgumentException, "Label '" << label << "' does not exist.");
uint64_t labelIndex = labelIt->second;
// Erase entry in map
nameToLabelingIndexMap.erase(labelIt);
// Erase label by 'swap and pop'
std::iter_swap(labelings.begin() + labelIndex, labelings.end() - 1);
labelings.pop_back();
// Update index of labeling we swapped from the end
for (auto& it: nameToLabelingIndexMap) {
if (it.second == labelings.size()) {
it.second = labelIndex;
break;
}
}
}
void ItemLabeling::join(ItemLabeling const& other) {
STORM_LOG_THROW(this->itemCount == other.itemCount, storm::exceptions::InvalidArgumentException, "The item count of the two labelings does not match: " << this->itemCount << " vs. " << other.itemCount << ".");
for (auto const& label : other.getLabels()) {
@ -123,11 +142,17 @@ namespace storm {
}
void ItemLabeling::addLabelToItem(std::string const& label, uint64_t item) {
STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::OutOfRangeException, "Label '" << label << "' unknown.");
STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "Label '" << label << "' unknown.");
STORM_LOG_THROW(item < itemCount, storm::exceptions::OutOfRangeException, "Item index out of range.");
this->labelings[nameToLabelingIndexMap.at(label)].set(item, true);
}
void ItemLabeling::removeLabelFromItem(std::string const& label, uint64_t item) {
STORM_LOG_THROW(item < itemCount, storm::exceptions::OutOfRangeException, "Item index out of range.");
STORM_LOG_THROW(this->getItemHasLabel(label, item),storm::exceptions::InvalidArgumentException, "Item " << item << " does not have label '" << label << "'.");
this->labelings[nameToLabelingIndexMap.at(label)].set(item, false);
}
bool ItemLabeling::getItemHasLabel(std::string const& label, uint64_t item) const {
STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label '" << label << "' is invalid for the labeling of the model.");
return this->labelings[nameToLabelingIndexMap.at(label)].get(item);

17
src/storm/models/sparse/ItemLabeling.h

@ -51,7 +51,6 @@ namespace storm {
*/
bool operator==(ItemLabeling const& other) const;
/*!
* Adds a new label to the labelings. Initially, no item is labeled with this label.
*
@ -59,6 +58,13 @@ namespace storm {
*/
void addLabel(std::string const& label);
/*!
* Removes a label from the labelings.
*
* @param label The name of the label to remove.
*/
void removeLabel(std::string const& label);
/*!
* Retrieves the set of labels contained in this labeling.
*
@ -191,7 +197,14 @@ namespace storm {
*/
virtual void addLabelToItem(std::string const& label, uint64_t item);
/*!
* Removes a label from a given item.
*
* @param label The name of the label to remove.
* @param item The index of the item.
*/
virtual void removeLabelFromItem(std::string const& label, uint64_t item);
// The number of items for which this object can hold the labeling.
uint64_t itemCount;

4
src/storm/models/sparse/MarkovAutomaton.cpp

@ -272,8 +272,8 @@ namespace storm {
//TODO update reward models and choice labels according to kept states
STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards.");
STORM_LOG_WARN_COND(!this->hasChoiceLabeling(), "Conversion of MA to CTMC does not preserve choice labels.");
STORM_LOG_WARN_COND(!this->hasStateValuations(), "Conversion of MA to CTMC does not preserve choice labels.");
STORM_LOG_WARN_COND(!this->hasChoiceOrigins(), "Conversion of MA to CTMC does not preserve choice labels.");
STORM_LOG_WARN_COND(!this->hasStateValuations(), "Conversion of MA to CTMC does not preserve state valuations.");
STORM_LOG_WARN_COND(!this->hasChoiceOrigins(), "Conversion of MA to CTMC does not preserve choice origins.");
return std::make_shared<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(rateMatrix), std::move(stateLabeling));
}

4
src/storm/models/sparse/StateLabeling.cpp

@ -52,6 +52,10 @@ namespace storm {
void StateLabeling::addLabelToState(std::string const& label, storm::storage::sparse::state_type state) {
ItemLabeling::addLabelToItem(label, state);
}
void StateLabeling::removeLabelFromState(std::string const& label, storm::storage::sparse::state_type state) {
ItemLabeling::removeLabelFromItem(label, state);
}
bool StateLabeling::getStateHasLabel(std::string const& label, storm::storage::sparse::state_type state) const {
return ItemLabeling::getItemHasLabel(label, state);

8
src/storm/models/sparse/StateLabeling.h

@ -65,6 +65,14 @@ namespace storm {
* @param state The index of the state to label.
*/
void addLabelToState(std::string const& label, storm::storage::sparse::state_type state);
/*!
* Removes a label from a given state.
*
* @param label The name of the label to remove.
* @param state The index of the state.
*/
void removeLabelFromState(std::string const& label, storm::storage::sparse::state_type state);
/*!
* Checks whether a given state is labeled with the given label.

2
src/storm/settings/SettingsManager.cpp

@ -39,6 +39,7 @@
#include "storm/settings/modules/MultiObjectiveSettings.h"
#include "storm/settings/modules/MultiplierSettings.h"
#include "storm/settings/modules/TransformationSettings.h"
#include "storm/settings/modules/HintSettings.h"
#include "storm/utility/macros.h"
#include "storm/utility/file.h"
#include "storm/utility/string.h"
@ -670,6 +671,7 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::MultiObjectiveSettings>();
storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
storm::settings::addModule<storm::settings::modules::TransformationSettings>();
storm::settings::addModule<storm::settings::modules::HintSettings>();
}
}

43
src/storm/settings/modules/HintSettings.cpp

@ -0,0 +1,43 @@
#include "storm/settings/modules/HintSettings.h"
#include "storm/settings/Option.h"
#include "storm/settings/OptionBuilder.h"
#include "storm/settings/ArgumentBuilder.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/IllegalArgumentValueException.h"
namespace storm {
namespace settings {
namespace modules {
const std::string HintSettings::moduleName = "hints";
const std::string stateHintOption = "states";
HintSettings::HintSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, stateHintOption, true,
"Estimate of the number of reachable states").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "size.").build()).build());
}
bool HintSettings::isNumberStatesSet() const {
return this->getOption(stateHintOption).getHasOptionBeenSet();
}
uint64_t HintSettings::getNumberStates() const {
return this->getOption(stateHintOption).getArgumentByName("number").getValueAsUnsignedInteger();
}
bool HintSettings::check() const {
return true;
}
void HintSettings::finalize() {
//Intentionally left empty
}
} // namespace modules
} // namespace settings
} // namespace storm

40
src/storm/settings/modules/HintSettings.h

@ -0,0 +1,40 @@
#pragma once
#include "storm-config.h"
#include "storm/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the model transformer settings
*/
class HintSettings : public ModuleSettings {
public:
/*!
* Creates a new set of transformer settings.
*/
HintSettings();
/*!
* Retrieves whether the option that estimates the number of states is set.
*/
bool isNumberStatesSet() const;
uint64_t getNumberStates() const;
bool check() const override;
void finalize() override;
// The name of the module.
static const std::string moduleName;
};
} // namespace modules
} // namespace settings
} // namespace storm

2
src/storm/solver/stateelimination/NondeterministicModelStateEliminator.h

@ -13,7 +13,7 @@ namespace storm {
NondeterministicModelStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& rowValues);
// Instantiaton of virtual methods.
// Instantiation of virtual methods.
virtual void updateValue(storm::storage::sparse::state_type const& row, ValueType const& loopProbability) override;
virtual void updatePredecessor(storm::storage::sparse::state_type const& predecessorRow, ValueType const& probability, storm::storage::sparse::state_type const& row) override;

5
src/storm/storage/BitVector.cpp

@ -1,17 +1,14 @@
#include <iostream>
#include <algorithm>
#include <bitset>
#include "storm/storage/BitVector.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/OutOfRangeException.h"
#include "storm/storage/BoostTypes.h"
#include "storm/utility/OsDetection.h"
#include "storm/utility/Hash.h"
#include "storm/utility/macros.h"
#include <bitset>
#ifdef STORM_DEV
#define ASSERT_BITVECTOR

178
src/storm/storage/BitVector.h

@ -10,7 +10,7 @@
namespace storm {
namespace storage {
/*!
* A bit vector that is internally represented as a vector of 64-bit values.
*/
@ -23,7 +23,7 @@ namespace storm {
class const_iterator : public std::iterator<std::input_iterator_tag, uint_fast64_t> {
// Declare the BitVector class as a friend class to access its internal storage.
friend class BitVector;
public:
/*!
* Constructs an iterator over the indices of the set bits in the given bit vector, starting and
@ -36,21 +36,21 @@ namespace storm {
* @param endIndex The index at which to abort the iteration process.
*/
const_iterator(uint64_t const* dataPtr, uint_fast64_t startIndex, uint_fast64_t endIndex, bool setOnFirstBit = true);
/*!
* Constructs an iterator by copying the given iterator.
*
* @param other The iterator to copy.
*/
const_iterator(const_iterator const& other);
/*!
* Assigns the contents of the given iterator to the current one via copying the former's contents.
*
* @param other The iterator from which to copy-assign.
*/
const_iterator& operator=(const_iterator const& other);
/*!
* Increases the position of the iterator to the position of the next bit that is set to true in the
* underlying bit vector.
@ -64,14 +64,14 @@ namespace storm {
* underlying bit vector.
*/
const_iterator& operator+=(size_t n);
/*!
* Returns the index of the current bit to which this iterator points.
*
* @return The index of the current bit to which this iterator points.
*/
uint_fast64_t operator*() const;
/*!
* Compares the iterator with another iterator for inequality.
*
@ -79,7 +79,7 @@ namespace storm {
* @return True if the two iterators are unequal.
*/
bool operator!=(const_iterator const& other) const;
/*!
* Compares the iterator with another iterator for equality.
*
@ -87,28 +87,28 @@ namespace storm {
* @return True if the two iterators are equal.
*/
bool operator==(const_iterator const& other) const;
private:
// The underlying bit vector of this iterator.
uint64_t const* dataPtr;
// The index of the bit this iterator currently points to.
uint_fast64_t currentIndex;
// The index of the bit that is past the end of the range of this iterator.
uint_fast64_t endIndex;
};
/*
/*!
* Constructs an empty bit vector of length 0.
*/
BitVector();
/*
/*!
* Deconstructs a bit vector by deleting the underlying storage.
*/
~BitVector();
/*!
* Constructs a bit vector which can hold the given number of bits and initializes all bits with the
* provided truth value.
@ -117,7 +117,7 @@ namespace storm {
* @param init The initial value of the first |length| bits.
*/
explicit BitVector(uint_fast64_t length, bool init = false);
/*!
* Creates a bit vector that has exactly the bits set that are given by the provided input iterator range
* [first, last).
@ -128,26 +128,26 @@ namespace storm {
*/
template<typename InputIterator>
BitVector(uint_fast64_t length, InputIterator first, InputIterator last);
/*!
* Creates a bit vector that has exactly the bits set that are given by the vector
*/
BitVector(uint_fast64_t length, std::vector<uint_fast64_t> setEntries);
/*!
* Performs a deep copy of the given bit vector.
*
* @param other A reference to the bit vector to be copied.
*/
BitVector(BitVector const& other);
/*!
* Move constructs the bit vector from the given bit vector.
*
* @param other The bit vector from which to move-construct.
*/
BitVector(BitVector&& other);
/*!
* Compares the given bit vector with the current one.
*
@ -155,7 +155,7 @@ namespace storm {
* @return True iff the other bit vector is semantically the same as the current one.
*/
bool operator==(BitVector const& other) const;
/*!
* Compares the given bit vector with the current one.
*
@ -163,7 +163,7 @@ namespace storm {
* @return True iff the other bit vector is semantically not the same as the current one.
*/
bool operator!=(BitVector const& other) const;
/*!
* Assigns the contents of the given bit vector to the current bit vector via a deep copy.
*
@ -172,7 +172,7 @@ namespace storm {
* deep copy.
*/
BitVector& operator=(BitVector const& other);
/*!
* Move assigns the given bit vector to the current bit vector.
*
@ -181,7 +181,7 @@ namespace storm {
* into it.
*/
BitVector& operator=(BitVector&& other);
/*!
* Retrieves whether the current bit vector is (in some order) smaller than the given one.
*
@ -189,15 +189,15 @@ namespace storm {
* @return True iff the current bit vector is smaller than the given one.
*/
bool operator<(BitVector const& other) const;
/*!
* Sets the given truth value at the given index.
*
* @param index The index where to set the truth value.
* @param value The truth value to set.
*/
void set(const uint_fast64_t index, bool value = true);
void set(uint_fast64_t index, bool value = true);
/*!
* Sets all bits in the given iterator range [first, last).
*
@ -206,7 +206,7 @@ namespace storm {
*/
template<typename InputIterator>
void set(InputIterator first, InputIterator last, bool value = true);
/*!
* Retrieves the truth value of the bit at the given index. Note: this does not check whether the given
* index is within bounds.
@ -215,7 +215,7 @@ namespace storm {
* @return True iff the bit at the given index is set.
*/
bool operator[](uint_fast64_t index) const;
/*!
* Retrieves the truth value of the bit at the given index and performs a bound check. If the access is
* out-of-bounds an OutOfBoundsException is thrown.
@ -223,8 +223,8 @@ namespace storm {
* @param index The index of the bit to access.
* @return True iff the bit at the given index is set.
*/
bool get(const uint_fast64_t index) const;
bool get(uint_fast64_t index) const;
/*!
* Resizes the bit vector to hold the given new number of bits. If the bit vector becomes smaller this way,
* the bits are truncated. Otherwise, the new bits are initialized to the given value.
@ -246,7 +246,7 @@ namespace storm {
* Expands the size to a multiple of 64.
*/
void expandSize(bool init = false);
/*!
* Enlarges the bit vector such that it holds at least the given number of bits (but possibly more).
* This can be used to diminish reallocations when the final size of the bit vector is not known yet.
@ -257,7 +257,7 @@ namespace storm {
* @param init The truth value to which to initialize newly created bits.
*/
void grow(uint_fast64_t minimumLength, bool init = false);
/*!
* Performs a logical "and" with the given bit vector. In case the sizes of the bit vectors do not match,
* only the matching portion is considered and the overlapping bits are set to 0.
@ -266,7 +266,7 @@ namespace storm {
* @return A bit vector corresponding to the logical "and" of the two bit vectors.
*/
BitVector operator&(BitVector const& other) const;
/*!
* Performs a logical "and" with the given bit vector and assigns the result to the current bit vector.
* In case the sizes of the bit vectors do not match, only the matching portion is considered and the
@ -277,7 +277,7 @@ namespace storm {
* of the two bit vectors.
*/
BitVector& operator&=(BitVector const& other);
/*!
* Performs a logical "or" with the given bit vector. In case the sizes of the bit vectors do not match,
* only the matching portion is considered and the overlapping bits are set to 0.
@ -286,7 +286,7 @@ namespace storm {
* @return A bit vector corresponding to the logical "or" of the two bit vectors.
*/
BitVector operator|(BitVector const& other) const;
/*!
* Performs a logical "or" with the given bit vector and assigns the result to the current bit vector.
* In case the sizes of the bit vectors do not match, only the matching portion is considered and the
@ -297,7 +297,7 @@ namespace storm {
* of the two bit vectors.
*/
BitVector& operator|=(BitVector const& other);
/*!
* Performs a logical "xor" with the given bit vector. In case the sizes of the bit vectors do not match,
* only the matching portion is considered and the overlapping bits are set to 0.
@ -306,36 +306,39 @@ namespace storm {
* @return A bit vector corresponding to the logical "xor" of the two bit vectors.
*/
BitVector operator^(BitVector const& other) const;
/*!
* Computes a bit vector that is as long as the number of set bits in the given filter that has bit i is set
* iff the i-th set bit of the current bit vector is set in the filter.
* Computes a bit vector that contains only the values of the bits given by the filter.
* The returned bit vector is as long as the number of set bits in the given filter.
* Bit i is set in the returned bit vector iff the i-th set bit of the current bit vector is set in the filter.
*
* For example: 00100110 % 10101010 returns 0101
*
* @param filter A reference the bit vector to use as the filter.
* @return A bit vector that is as long as the number of set bits in the given filter that has bit i is set
* iff the i-th set bit of the current bit vector is set in the filter.
* @param filter A reference bit vector to use as the filter.
* @return A bit vector that is as long as the number of set bits in the given filter and
* contains only the values of the bits set in the filter.
*/
BitVector operator%(BitVector const& filter) const;
/*!
* Performs a logical "not" on the bit vector.
*
* @return A bit vector corresponding to the logical "not" of the bit vector.
*/
BitVector operator~() const;
/*!
* Negates all bits in the bit vector.
*/
void complement();
/*!
* Increments the (unsigned) number represented by this BitVector by one.
* @note Index 0 is assumed to be the least significant bit.
* @note Wraps around, i.e., incrementing 11..1 yields 00..0.
*/
void increment();
/*!
* Performs a logical "implies" with the given bit vector. In case the sizes of the bit vectors do not
* match, only the matching portion is considered and the overlapping bits are set to 0.
@ -344,7 +347,7 @@ namespace storm {
* @return A bit vector corresponding to the logical "implies" of the two bit vectors.
*/
BitVector implies(BitVector const& other) const;
/*!
* Checks whether all bits that are set in the current bit vector are also set in the given bit vector.
*
@ -354,7 +357,7 @@ namespace storm {
* vector.
*/
bool isSubsetOf(BitVector const& other) const;
/*!
* Checks whether none of the bits that are set in the current bit vector are also set in the given bit
* vector.
@ -365,7 +368,7 @@ namespace storm {
* given bit vector.
*/
bool isDisjointFrom(BitVector const& other) const;
/*!
* Checks whether the given bit vector matches the bits starting from the given index in the current bit
* vector. Note: the given bit vector must be shorter than the current one minus the given index.
@ -375,7 +378,7 @@ namespace storm {
* @return bool True iff the bits match exactly.
*/
bool matches(uint_fast64_t bitIndex, BitVector const& other) const;
/*!
* Sets the exact bit pattern of the given bit vector starting at the given bit index. Note: the given bit
* vector must be shorter than the current one minus the given index.
@ -393,7 +396,7 @@ namespace storm {
* TODO this operation is slow.
*/
BitVector permute(std::vector<uint64_t> const& inversePermutation) const;
/*!
* Retrieves the content of the current bit vector at the given index for the given number of bits as a new
* bit vector.
@ -403,7 +406,7 @@ namespace storm {
* @return A new bit vector holding the selected bits.
*/
storm::storage::BitVector get(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const;
/*!
* Retrieves the content of the current bit vector at the given index for the given number of bits as an
* unsigned integer value.
@ -412,14 +415,14 @@ namespace storm {
* @param numberOfBits The number of bits to get. This value must be less or equal than 64.
*/
uint_fast64_t getAsInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const;
/*!
*
* @param bitIndex The index of the first of the two bits to get
* @return A value between 0 and 3, encoded as a byte.
*/
uint_fast64_t getTwoBitsAligned(uint_fast64_t bitIndex) const;
/*!
* Sets the selected number of lowermost bits of the provided value at the given bit index.
*
@ -428,14 +431,14 @@ namespace storm {
* @param value The integer whose lowermost bits to set.
*/
void setFromInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits, uint64_t value);
/*!
* Retrieves whether no bits are set to true in this bit vector.
*
* @return False iff there is at least one bit set in this vector.
*/
bool empty() const;
/*!
* Retrieves whether all bits are set in this bit vector.
* If the bit vector has size 0, this method always returns true.
@ -443,24 +446,24 @@ namespace storm {
* @return True iff all bits in the bit vector are set.
*/
bool full() const;
/*!
* Removes all set bits from the bit vector. Calling empty() after this operation will yield true.
*/
void clear();
/*!
* Sets all bits from the bit vector. Calling full() after this operation will yield true.
*/
void fill();
/*!
* Returns the number of bits that are set to true in this bit vector.
*
* @return The number of bits that are set to true in this bit vector.
*/
uint_fast64_t getNumberOfSetBits() const;
/*!
* Retrieves the number of bits set in this bit vector with an index strictly smaller than the given one.
*
@ -468,39 +471,39 @@ namespace storm {
* @return The number of bits set in this bit vector with an index strictly smaller than the given one.
*/
uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const;
/*!
* Retrieves a vector that holds at position i the number of bits set before index i.
*
* @return The resulting vector of 'offsets'.
*/
std::vector<uint_fast64_t> getNumberOfSetBitsBeforeIndices() const;
/*!
* Retrieves the number of bits this bit vector can store.
*
* @return The number of bits this bit vector can hold.
*/
size_t size() const;
/*!
* Returns (an approximation of) the size of the bit vector measured in bytes.
*
* @return The size of the bit vector measured in bytes.
*/
std::size_t getSizeInBytes() const;
/*!
* Returns an iterator to the indices of the set bits in the bit vector.
*/
const_iterator begin() const;
/*!
* Returns an iterator pointing at the element past the bit vector.
*/
const_iterator end() const;
/*
/*!
* Retrieves the index of the bit that is the next bit set to true in the bit vector. If there is none,
* this function returns the number of bits this vector holds in total. Put differently, if the return
* value is equal to a call to size(), then there is no bit set after the specified position.
@ -510,8 +513,8 @@ namespace storm {
* @return The index of the next bit that is set after the given index.
*/
uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const;
/*
/*!
* Retrieves the index of the bit that is the next bit set to false in the bit vector. If there is none,
* this function returns the number of bits this vector holds in total. Put differently, if the return
* value is equal to a call to size(), then there is no unset bit after the specified position.
@ -521,8 +524,8 @@ namespace storm {
* @return The index of the next bit that is set after the given index.
*/
uint_fast64_t getNextUnsetIndex(uint_fast64_t startingIndex) const;
/*
/*!
* Compare two intervals [start1, start1+length] and [start2, start2+length] and swap them if the second
* one is larger than the first one. After the method the intervals are sorted in decreasing order.
*
@ -532,14 +535,15 @@ namespace storm {
* @return True, if the intervals were swapped, false if nothing changed.
*/
bool compareAndSwap(uint_fast64_t start1, uint_fast64_t start2, uint_fast64_t length);
friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector);
friend struct std::hash<storm::storage::BitVector>;
friend struct FNV1aBitVectorHash;
template<typename StateType>
friend struct Murmur3BitVectorHash;
private:
/*!
* Creates an empty bit vector with the given number of buckets.
@ -548,7 +552,7 @@ namespace storm {
* @param bitCount This must be the number of buckets times 64.
*/
BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount);
/*!
* Retrieves the index of the next bit that is set to the given value after (and including) the given starting index.
*
@ -560,12 +564,12 @@ namespace storm {
* in the given bit vector or endIndex in case the end index was reached.
*/
static uint_fast64_t getNextIndexWithValue(bool value, uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex);
/*!
* Truncate the last bucket so that no bits are set starting from bitCount.
*/
void truncateLastBucket();
/*! Retrieves the content of the current bit vector at the given index for the given number of bits as a new
* bit vector.
*
@ -574,7 +578,7 @@ namespace storm {
* @return A new bit vector holding the selected bits.
*/
BitVector getAsBitVector(uint_fast64_t start, uint_fast64_t length) const;
/*!
* Sets the exact bit pattern of the given bit vector starting at the given bit index. Note: the given bit
* vector must be shorter than the current one minus the given index.
@ -583,31 +587,31 @@ namespace storm {
* @param other The bit vector whose pattern to set.
*/
void setFromBitVector(uint_fast64_t start, BitVector const& other);
/*!
* Print bit vector and display all bits.
*
* @param out Stream to print to.
*/
void printBits(std::ostream& out) const;
/*!
* Retrieves the number of buckets of the underlying storage.
*
* @return The number of buckets of the underlying storage.
*/
size_t bucketCount() const;
// The number of bits that this bit vector can hold.
uint_fast64_t bitCount;
// The underlying storage of 64-bit buckets for all bits of this bit vector.
uint64_t* buckets;
// A bit mask that can be used to reduce a modulo 64 operation to a logical "and".
static const uint_fast64_t mod64mask = (1 << 6) - 1;
};
struct FNV1aBitVectorHash {
std::size_t operator()(storm::storage::BitVector const& bv) const;
};
@ -621,7 +625,7 @@ namespace storm {
} // namespace storm
namespace std {
template <>
template<>
struct hash<storm::storage::BitVector> {
std::size_t operator()(storm::storage::BitVector const& bv) const;
};

8
src/storm/storage/jani/Model.cpp

@ -676,6 +676,14 @@ namespace storm {
return res;
}
std::size_t Model::getTotalNumberOfNonTransientVariables() const {
std::size_t res = globalVariables.getNumberOfNontransientVariables();
for (auto const& aut : getAutomata()) {
res += aut.getVariables().getNumberOfNontransientVariables();
}
return res;
}
Variable const& Model::addVariable(Variable const& variable) {
if (variable.isBooleanVariable()) {
return addVariable(variable.asBooleanVariable());

10
src/storm/storage/jani/Model.h

@ -384,7 +384,13 @@ namespace storm {
* Retrieves the total number of edges in this model.
*/
std::size_t getNumberOfEdges() const;
/*!
* Number of global and local variables.
*/
std::size_t getTotalNumberOfNonTransientVariables() const;
/*!
* Sets the system composition expression of the JANI model.
*/
@ -547,7 +553,7 @@ namespace storm {
* Determines whether this model is a discrete-time model.
*/
bool isDiscreteTimeModel() const;
/*!
* Retrieves a list of expressions that characterize the legal values of the variables in this model.
*

14
src/storm/storage/jani/VariableSet.cpp

@ -76,7 +76,8 @@ namespace storm {
}
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Cannot add variable of unknown type.");
}
BooleanVariable const& VariableSet::addVariable(BooleanVariable const& variable) {
STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
std::shared_ptr<BooleanVariable> newVariable = std::make_shared<BooleanVariable>(variable);
@ -321,7 +322,16 @@ namespace storm {
bool VariableSet::empty() const {
return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables() || containsRealVariables() || containsArrayVariables() || containsClockVariables());
}
uint64_t VariableSet::getNumberOfVariables() const {
return variables.size();
}
uint64_t VariableSet::getNumberOfNontransientVariables() const {
return getNumberOfVariables() - getNumberOfTransientVariables();
}
uint_fast64_t VariableSet::getNumberOfTransientVariables() const {
uint_fast64_t result = 0;
for (auto const& variable : variables) {

20
src/storm/storage/jani/VariableSet.h

@ -228,26 +228,36 @@ namespace storm {
* Retrieves whether this variable set is empty.
*/
bool empty() const;
/*!
* Total number of variables, including transient variables.
*/
uint64_t getNumberOfVariables() const;
/*
* Total number of nontransient variables
*/
uint64_t getNumberOfNontransientVariables() const;
/*!
* Retrieves the number of transient variables in this variable set.
*/
uint_fast64_t getNumberOfTransientVariables() const;
uint64_t getNumberOfTransientVariables() const;
/*!
* Retrieves the number of real transient variables in this variable set.
*/
uint_fast64_t getNumberOfRealTransientVariables() const;
uint64_t getNumberOfRealTransientVariables() const;
/*!
* Retrieves the number of unbounded integer transient variables in this variable set.
*/
uint_fast64_t getNumberOfUnboundedIntegerTransientVariables() const;
uint64_t getNumberOfUnboundedIntegerTransientVariables() const;
/*!
* Retrieves the number of numerical (i.e. real, or integer) transient variables in this variable set.
*/
uint_fast64_t getNumberOfNumericalTransientVariables() const;
uint64_t getNumberOfNumericalTransientVariables() const;
/*!
* Retrieves the transient variables in this variable set.

20
src/storm/storage/jani/traverser/InformationCollector.cpp

@ -0,0 +1,20 @@
#include "storm/storage/jani/traverser/InformationCollector.h"
#include "storm/storage/jani/traverser/JaniTraverser.h"
#include "storm/storage/jani/Model.h"
namespace storm {
namespace jani {
namespace detail {
}
InformationObject collect(Model const& model) {
InformationObject result;
result.modelType = model.getModelType();
result.nrAutomata = model.getNumberOfAutomata();
result.nrEdges = model.getNumberOfEdges();
result.nrVariables = model.getTotalNumberOfNonTransientVariables();
return result;
}
}
}

20
src/storm/storage/jani/traverser/InformationCollector.h

@ -0,0 +1,20 @@
#pragma once
#include "storm/storage/jani/ModelType.h"
namespace storm {
namespace jani {
class Model;
struct InformationObject {
storm::jani::ModelType modelType;
uint64_t nrVariables;
uint64_t nrAutomata;
uint64_t nrEdges;
uint64_t nrLocations;
};
InformationObject collect(Model const& model);
}
}

357
src/storm/transformer/NonMarkovianChainTransformer.cpp

@ -1,40 +1,35 @@
#include <queue>
#include "NonMarkovianChainTransformer.h"
#include "storm/logic/Formulas.h"
#include "storm/logic/FragmentSpecification.h"
#include <queue>
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/exceptions/InvalidModelException.h"
#include "storm/logic/Formulas.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/models/sparse/Ctmc.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include <storm/solver/stateelimination/NondeterministicModelStateEliminator.h>
#include "storm/storage/FlexibleSparseMatrix.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/utility/constants.h"
#include "storm/utility/ConstantsComparator.h"
#include "storm/utility/vector.h"
#include "storm/utility/macros.h"
#include "storm/utility/graph.h"
namespace storm {
namespace transformer {
template<typename ValueType, typename RewardModelType>
std::shared_ptr<models::sparse::Model<ValueType, RewardModelType>>
NonMarkovianChainTransformer<ValueType, RewardModelType>::eliminateNonmarkovianStates(
std::shared_ptr<models::sparse::MarkovAutomaton<ValueType, RewardModelType>> ma,
EliminationLabelBehavior labelBehavior) {
// TODO reward models
NonMarkovianChainTransformer<ValueType, RewardModelType>::eliminateNonmarkovianStates(std::shared_ptr<models::sparse::MarkovAutomaton<ValueType, RewardModelType>> ma,
EliminationLabelBehavior labelBehavior) {
STORM_LOG_WARN_COND(labelBehavior == EliminationLabelBehavior::KeepLabels, "Labels are not preserved! Results may be incorrect. Continue at your own caution.");
if (labelBehavior == EliminationLabelBehavior::DeleteLabels) {
STORM_PRINT("Use Label Deletion" << std::endl)
}
if (labelBehavior == EliminationLabelBehavior::MergeLabels) {
STORM_PRINT("Use Label Merging" << std::endl)
}
STORM_LOG_WARN("Reward Models and Choice Labelings are ignored!");
if (ma->isClosed() && ma->getMarkovianStates().full()) {
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> components(
ma->getTransitionMatrix(), ma->getStateLabeling(), ma->getRewardModels(), false);
STORM_LOG_THROW(ma->isClosed(), storm::exceptions::InvalidModelException, "MA should be closed first.");
if (ma->getMarkovianStates().full()) {
// Is already a CTMC
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> components(ma->getTransitionMatrix(), ma->getStateLabeling(), ma->getRewardModels(), false);
components.exitRates = ma->getExitRates();
if (ma->hasChoiceLabeling()) {
components.choiceLabeling = ma->getChoiceLabeling();
@ -45,243 +40,98 @@ namespace storm {
if (ma->hasChoiceOrigins()) {
components.choiceOrigins = ma->getChoiceOrigins();
}
return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>(
std::move(components));
return std::make_shared<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(components));
}
std::map<uint_fast64_t, uint_fast64_t> eliminationMapping;
std::set<uint_fast64_t> statesToKeep;
std::queue<uint_fast64_t> changedStates;
std::queue<uint_fast64_t> queue;
storm::storage::SparseMatrix<ValueType> backwards = ma->getBackwardTransitions();
// Initialize
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(ma->getTransitionMatrix());
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(ma->getTransitionMatrix().transpose(), true);
storm::models::sparse::StateLabeling stateLabeling = ma->getStateLabeling();
// TODO: update reward models and choice labels according to kept states
STORM_LOG_WARN_COND(ma->getRewardModels().empty(), "Reward models are not preserved in chain elimination.");
std::unordered_map<std::string, RewardModelType> rewardModels;
STORM_LOG_WARN_COND(!ma->hasChoiceLabeling(), "Choice labels are not preserved in chain elimination.");
STORM_LOG_WARN_COND(!ma->hasStateValuations(), "State valuations are not preserved in chain elimination.");
STORM_LOG_WARN_COND(!ma->hasChoiceOrigins(), "Choice origins are not preserved in chain elimination.");
// Eliminate all probabilistic states by state elimination
auto actionRewards = std::vector<ValueType>(ma->getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
storm::solver::stateelimination::NondeterministicModelStateEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, actionRewards);
storm::storage::BitVector keepStates(ma->getNumberOfStates(), true);
// Determine the state remapping
for (uint_fast64_t base_state = 0; base_state < ma->getNumberOfStates(); ++base_state) {
STORM_LOG_ASSERT(!ma->isHybridState(base_state), "Base state is hybrid.");
if (ma->isMarkovianState(base_state)) {
queue.push(base_state);
while (!queue.empty()) {
auto currState = queue.front();
queue.pop();
auto currLabels = ma->getLabelsOfState(currState);
// Get predecessors from matrix
typename storm::storage::SparseMatrix<ValueType>::rows entriesInRow = backwards.getRow(currState);
for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) {
uint_fast64_t predecessor = entryIt->getColumn();
if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) {
if (labelBehavior == EliminationLabelBehavior::DeleteLabels || labelBehavior == EliminationLabelBehavior::MergeLabels ||
currLabels == ma->getLabelsOfState(predecessor)) {
// If labels are not to be preserved or states are labeled the same
if (!eliminationMapping.count(predecessor)) {
eliminationMapping[predecessor] = base_state;
queue.push(predecessor);
} else if (eliminationMapping[predecessor] != base_state) {
eliminationMapping.erase(predecessor);
statesToKeep.insert(predecessor);
changedStates.push(predecessor);
}
} else {
// Labels are to be preserved and states have different labels
if (eliminationMapping.count(predecessor)) {
eliminationMapping.erase(predecessor);
}
statesToKeep.insert(predecessor);
changedStates.push(predecessor);
for (uint_fast64_t state = 0; state < ma->getNumberOfStates(); ++state) {
STORM_LOG_ASSERT(!ma->isHybridState(state), "State is hybrid.");
if (ma->isProbabilisticState(state)) {
// Only eliminate immediate states (and no Markovian states)
if (ma->getNumberOfChoices(state) <= 1) {
// Eliminate only if no non-determinism occurs
STORM_LOG_ASSERT(ma->getNumberOfChoices(state) == 1, "State " << state << " has no choices.");
STORM_LOG_ASSERT(flexibleMatrix.getRowGroupSize(state) == 1, "State " << state << " has too many rows.");
if (labelBehavior == EliminationLabelBehavior::KeepLabels) {
// Only eliminate if eliminated state and all its successors have the same labels
bool sameLabels = true;
auto currLabels = stateLabeling.getLabelsOfState(state);
typename storm::storage::FlexibleSparseMatrix<ValueType>::row_type entriesInRow = flexibleMatrix.getRow(state, 0); // Row group
for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) {
if (currLabels != stateLabeling.getLabelsOfState(entryIt->getColumn())) {
STORM_LOG_TRACE("Do not eliminate state " << state << " because labels of state " << entryIt->getColumn() << " are different.");
sameLabels = false;
break;
}
}
}
}
}
}
// Correct the mapping with the states which have to be kept
while (!changedStates.empty()) {
uint_fast64_t base_state = changedStates.front();
queue.push(base_state);
while (!queue.empty()) {
auto currState = queue.front();
queue.pop();
auto currLabels = ma->getLabelsOfState(currState);
if (!sameLabels) {
continue;
}
} else {
// As helper for the labeling we create a bitvector representing all successor states
storm::storage::BitVector successors(stateLabeling.getNumberOfItems());
typename storm::storage::FlexibleSparseMatrix<ValueType>::row_type entriesInRow = flexibleMatrix.getRow(state, 0); // Row group
for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) {
successors.set(entryIt->getColumn());
}
// Get predecessors from matrix
typename storm::storage::SparseMatrix<ValueType>::rows entriesInRow = backwards.getRow(currState);
for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) {
uint_fast64_t predecessor = entryIt->getColumn();
if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) {
if (labelBehavior == EliminationLabelBehavior::DeleteLabels || labelBehavior == EliminationLabelBehavior::MergeLabels ||
currLabels == ma->getLabelsOfState(predecessor)) {
// If labels are not to be preserved or states are labeled the same
if (!eliminationMapping.count(predecessor)) {
eliminationMapping[predecessor] = base_state;
queue.push(predecessor);
} else if (eliminationMapping[predecessor] != base_state) {
eliminationMapping.erase(predecessor);
statesToKeep.insert(predecessor);
changedStates.push(predecessor);
if (labelBehavior == EliminationLabelBehavior::MergeLabels) {
// Add labels from eliminated state to successors
for (std::string const& label : stateLabeling.getLabelsOfState(state)) {
storm::storage::BitVector states = stateLabeling.getStates(label);
// Add successor states for this label as well
stateLabeling.setStates(label, states | successors);
}
} else {
// Labels are to be preserved and states have different labels
if (eliminationMapping.count(predecessor)) {
eliminationMapping.erase(predecessor);
STORM_LOG_ASSERT(labelBehavior == EliminationLabelBehavior::DeleteLabels, "Unknown label behavior.");
if (stateLabeling.getStateHasLabel("init", state)) {
// Add "init" label of eliminated state to successor states
storm::storage::BitVector states = stateLabeling.getStates("init");
// Add successor states for this label as well
stateLabeling.setStates("init", states | successors);
}
statesToKeep.insert(predecessor);
changedStates.push(predecessor);
}
}
}
}
changedStates.pop();
}
// At this point, we hopefully have a valid mapping which eliminates a lot of states
STORM_LOG_TRACE("Elimination Mapping:");
for (auto entry : eliminationMapping) {
STORM_LOG_TRACE(std::to_string(entry.first) << " -> " << std::to_string(entry.second));
}
STORM_LOG_INFO("Eliminating " << eliminationMapping.size() << " states" << std::endl);
// TODO explore if one can construct elimination mapping and state remapping in one step
uint64_t newStateCount = ma->getNumberOfStates() - eliminationMapping.size();
std::vector<std::set<std::string>> labelMap(newStateCount, std::set<std::string>());
// Construct a mapping of old state space to new one
std::vector<uint_fast64_t> stateRemapping(ma->getNumberOfStates(), -1);
uint_fast64_t currentNewState = 0;
for (uint_fast64_t state = 0; state < ma->getNumberOfStates(); ++state) {
if (eliminationMapping.count(state) > 0) {
if (stateRemapping[eliminationMapping[state]] == uint_fast64_t(-1)) {
stateRemapping[eliminationMapping[state]] = currentNewState;
stateRemapping[state] = currentNewState;
++currentNewState;
queue.push(eliminationMapping[state]);
} else {
stateRemapping[state] = stateRemapping[eliminationMapping[state]];
}
if (labelBehavior == EliminationLabelBehavior::DeleteLabels && ma->getInitialStates().get(state)) {
// Keep initial label for 'delete' behavior
labelMap[stateRemapping[eliminationMapping[state]]].insert("init");
}
if (labelBehavior == EliminationLabelBehavior::MergeLabels) {
//add all labels to the label set for the representative
for (auto const &label : ma->getLabelsOfState(state)) {
labelMap[stateRemapping[eliminationMapping[state]]].insert(label);
}
}
} else {
if (stateRemapping[state] == uint_fast64_t(-1)) {
stateRemapping[state] = currentNewState;
queue.push(state);
++currentNewState;
}
if (labelBehavior == EliminationLabelBehavior::DeleteLabels && ma->getInitialStates().get(state)) {
// Keep initial label for 'delete' behavior
labelMap[stateRemapping[state]].insert("init");
}
if (labelBehavior == EliminationLabelBehavior::MergeLabels) {
for (auto const &label : ma->getLabelsOfState(state)) {
labelMap[stateRemapping[state]].insert(label);
}
// Eliminate this probabilistic state
stateEliminator.eliminateState(state, true);
keepStates.set(state, false);
}
}
}
// Build the new MA
storm::storage::SparseMatrix<ValueType> newTransitionMatrix;
storm::models::sparse::StateLabeling newStateLabeling(newStateCount);
storm::storage::BitVector newMarkovianStates(ma->getNumberOfStates() - eliminationMapping.size(),false);
std::vector<ValueType> newExitRates;
//TODO choice labeling
boost::optional<storm::models::sparse::ChoiceLabeling> newChoiceLabeling;
// Create the new matrix
auto keptRows = ma->getTransitionMatrix().getRowFilter(keepStates);
storm::storage::SparseMatrix<ValueType> matrix = flexibleMatrix.createSparseMatrix(keptRows, keepStates);
// Initialize the matrix builder and helper variables
storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(
0, 0, 0, false, true, 0);
// TODO: obtain the reward model for the resulting system
for (auto const &label : ma->getStateLabeling().getLabels()) {
if (!newStateLabeling.containsLabel(label)) {
newStateLabeling.addLabel(label);
}
}
uint_fast64_t currentRow = 0;
uint_fast64_t state = 0;
while (!queue.empty()) {
state = queue.front();
queue.pop();
// Prepare model components
storm::storage::BitVector markovianStates = ma->getMarkovianStates() % keepStates;
storm::models::sparse::StateLabeling labeling = stateLabeling.getSubLabeling(keepStates);
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> components(matrix, labeling, ma->getRewardModels(), false, markovianStates);
std::vector<ValueType> exitRates(markovianStates.size());
storm::utility::vector::selectVectorValues(exitRates, keepStates, ma->getExitRates());
components.exitRates = exitRates;
std::set<std::string> labelSet = ma->getLabelsOfState(state);
if (labelBehavior == EliminationLabelBehavior::DeleteLabels) {
labelSet.insert(labelMap[stateRemapping[state]].begin(), labelMap[stateRemapping[state]].end());
}
if (labelBehavior == EliminationLabelBehavior::MergeLabels) {
labelSet = labelMap[stateRemapping[state]];
}
for (auto const &label : labelSet) {
if (!newStateLabeling.containsLabel(label)) {
newStateLabeling.addLabel(label);
}
newStateLabeling.addLabelToState(label, stateRemapping[state]);
}
// Use a set to not include redundant rows
std::set<std::map<uint_fast64_t, ValueType>> rowSet;
for (uint_fast64_t row = 0; row < ma->getTransitionMatrix().getRowGroupSize(state); ++row) {
std::map<uint_fast64_t, ValueType> transitions;
for (typename storm::storage::SparseMatrix<ValueType>::const_iterator itEntry = ma->getTransitionMatrix().getRow(
state, row).begin();
itEntry != ma->getTransitionMatrix().getRow(state, row).end(); ++itEntry) {
uint_fast64_t newId = stateRemapping[itEntry->getColumn()];
if (transitions.count(newId) == 0) {
transitions[newId] = itEntry->getValue();
} else {
transitions[newId] += itEntry->getValue();
}
}
rowSet.insert(transitions);
}
// correctly set rates
auto rate = storm::utility::zero<ValueType>();
if (ma->isMarkovianState(state)) {
newMarkovianStates.set(stateRemapping[state], true);
rate = ma->getExitRates().at(state);
}
newExitRates.push_back(rate);
// Build matrix
matrixBuilder.newRowGroup(currentRow);
for (auto const &row : rowSet) {
for (auto const &transition : row) {
matrixBuilder.addNextValue(currentRow, transition.first, transition.second);
STORM_LOG_TRACE(stateRemapping[state] << "->" << transition.first << " : " << transition.second
<< std::endl);
}
++currentRow;
}
}
// explicitly force dimensions of the matrix in case a column is missing
newTransitionMatrix = matrixBuilder.build(newStateCount, newStateCount, newStateCount);
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> newComponents = storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(
std::move(newTransitionMatrix), std::move(newStateLabeling));
newComponents.rateTransitions = false;
newComponents.markovianStates = std::move(newMarkovianStates);
newComponents.exitRates = std::move(newExitRates);
auto model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType >>(
std::move(newComponents));
// Build transformed model
auto model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>(std::move(components));
if (model->isConvertibleToCtmc()) {
return model->convertToCtmc();
} else {
@ -290,50 +140,49 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType>
bool NonMarkovianChainTransformer<ValueType, RewardModelType>::preservesFormula(
storm::logic::Formula const &formula) {
bool NonMarkovianChainTransformer<ValueType, RewardModelType>::preservesFormula(storm::logic::Formula const& formula) {
storm::logic::FragmentSpecification fragment = storm::logic::propositional();
fragment.setProbabilityOperatorsAllowed(true);
fragment.setGloballyFormulasAllowed(true);
fragment.setReachabilityProbabilityFormulasAllowed(true);
fragment.setUntilFormulasAllowed(true);
fragment.setBoundedUntilFormulasAllowed(true);
fragment.setTimeBoundedUntilFormulasAllowed(true);
fragment.setNextFormulasAllowed(false);
fragment.setStepBoundedUntilFormulasAllowed(false);
return formula.isInFragment(fragment);
}
template<typename ValueType, typename RewardModelType>
std::vector<std::shared_ptr<storm::logic::Formula const>>
NonMarkovianChainTransformer<ValueType, RewardModelType>::checkAndTransformFormulas(
std::vector<std::shared_ptr<storm::logic::Formula const>> const &formulas) {
NonMarkovianChainTransformer<ValueType, RewardModelType>::checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
std::vector<std::shared_ptr<storm::logic::Formula const>> result;
for (auto const &f : formulas) {
for (auto const& f : formulas) {
if (preservesFormula(*f)) {
result.push_back(f);
} else {
STORM_LOG_INFO("Non-Markovian chain elimination does not preserve formula " << *f);
STORM_LOG_WARN("Non-Markovian chain elimination does not preserve formula " << *f);
}
}
return result;
}
template
class NonMarkovianChainTransformer<double>;
template class NonMarkovianChainTransformer<double>;
template
class NonMarkovianChainTransformer<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
#ifdef STORM_HAVE_CARL
template class NonMarkovianChainTransformer<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template
class NonMarkovianChainTransformer<storm::RationalFunction>;
#ifdef STORM_HAVE_CARL
template class NonMarkovianChainTransformer<storm::RationalFunction>;
template
class NonMarkovianChainTransformer<storm::RationalNumber>;
template class NonMarkovianChainTransformer<storm::RationalNumber>;
#endif
}
}

7
src/storm/transformer/NonMarkovianChainTransformer.h

@ -21,13 +21,10 @@ namespace storm {
* If no non-determinism occurs, a CTMC is generated.
*
* @param ma The input Markov Automaton.
* @param preserveLabels If set, the procedure considers the labels of non-Markovian states when eliminating states.
* @param labelBehavior How the labels of non-Markovian states should be treated when eliminating states.
* @return A reference to the new model after eliminating non-Markovian states.
*/
static std::shared_ptr<models::sparse::Model<ValueType, RewardModelType>> eliminateNonmarkovianStates(
std::shared_ptr<models::sparse::MarkovAutomaton < ValueType, RewardModelType>> ma,
EliminationLabelBehavior labelBehavior = EliminationLabelBehavior::KeepLabels
);
static std::shared_ptr<models::sparse::Model<ValueType, RewardModelType>> eliminateNonmarkovianStates(std::shared_ptr<models::sparse::MarkovAutomaton<ValueType, RewardModelType>> ma, EliminationLabelBehavior labelBehavior = EliminationLabelBehavior::KeepLabels);
/**
* Check if the property specified by the given formula is preserved by the transformation.

4
src/storm/utility/DirectEncodingExporter.cpp

@ -63,6 +63,7 @@ namespace storm {
}
os << std::endl;
os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl;
os << "@nr_choices" << std::endl << sparseModel->getNumberOfChoices() << std::endl;
os << "@model" << std::endl;
storm::storage::SparseMatrix<ValueType> const& matrix = sparseModel->getTransitionMatrix();
@ -125,6 +126,9 @@ namespace storm {
if (sparseModel->hasChoiceLabeling()) {
os << "\taction ";
bool lfirst = true;
if (sparseModel->getChoiceLabeling().getLabelsOfChoice(row).empty()) {
os << "__NOLABEL__";
}
for (auto const& label : sparseModel->getChoiceLabeling().getLabelsOfChoice(row)) {
if (!lfirst) {
os << "_";

37
src/test/storm/model/StateLabelingTest.cpp

@ -0,0 +1,37 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm/models/sparse/StateLabeling.h"
TEST(StateLabelingTest, RemoveLabel) {
storm::models::sparse::StateLabeling labeling(10);
EXPECT_EQ(10ul, labeling.getNumberOfItems());
EXPECT_EQ(0ul, labeling.getNumberOfLabels());
storm::storage::BitVector statesTest1 = storm::storage::BitVector(10, {1, 4, 6, 7});
labeling.addLabel("test1", statesTest1);
EXPECT_TRUE(labeling.containsLabel("test1"));
EXPECT_FALSE(labeling.containsLabel("abc"));
storm::storage::BitVector statesTest2 = storm::storage::BitVector(10, {2, 6, 7, 8, 9});
labeling.addLabel("test2", statesTest2);
EXPECT_FALSE(labeling.getStateHasLabel("test2", 5));
labeling.addLabelToState("test2", 5);
EXPECT_TRUE(labeling.getStateHasLabel("test2", 5));
EXPECT_TRUE(labeling.getStateHasLabel("test1", 4));
labeling.removeLabelFromState("test1", 4);
EXPECT_FALSE(labeling.getStateHasLabel("test1", 4));
EXPECT_EQ(2ul, labeling.getNumberOfLabels());
EXPECT_TRUE(labeling.getStateHasLabel("test1", 6));
labeling.removeLabel("test1");
EXPECT_FALSE(labeling.containsLabel("test1"));
EXPECT_EQ(1ul, labeling.getNumberOfLabels());
EXPECT_TRUE(labeling.getStateHasLabel("test2", 5));
}

249
src/test/storm/transformer/NonMarkovianChainTransformerTest.cpp

@ -0,0 +1,249 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm/api/storm.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm-parsers/api/storm-parsers.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/storage/jani/Property.h"
TEST(NonMarkovianChainTransformerTest, StreamExampleTest) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma");
std::string formulasString = "Pmin=? [ F \"done\"];Pmin=? [ F<=1 \"done\"];Tmin=? [ F \"done\" ]";
auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
auto model = storm::api::buildSparseModel<double>(program, formulas)->template as<storm::models::sparse::MarkovAutomaton<double>>();
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(14ul, model->getNumberOfTransitions());
ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
size_t initState = 0;
auto labeling = model->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
ASSERT_TRUE(labeling.getStateHasLabel("done", 10));
auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[1], true));
EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[2], true));
EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
// Keep labels
auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels);
ASSERT_EQ(9ul, transformed.first->getNumberOfStates());
ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions());
labeling = transformed.first->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
ASSERT_TRUE(labeling.getStateHasLabel("done", 8));
EXPECT_EQ(2ul, transformed.second.size());
result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
//result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
//EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
// Merge labels
transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels);
ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
labeling = transformed.first->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
ASSERT_TRUE(labeling.getStateHasLabel("done", 7));
EXPECT_EQ(2ul, transformed.second.size());
result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
//result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
//EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
// Delete labels
transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels);
ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
labeling = transformed.first->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
ASSERT_TRUE(labeling.getStateHasLabel("done", 7));
EXPECT_EQ(2ul, transformed.second.size());
result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
//result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
//EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
}
TEST(NonMarkovianChainTransformerTest, ChainElimination1ExampleTest) {
auto model = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination1.drn")->template as<storm::models::sparse::MarkovAutomaton<double>>();
std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]";
auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString));
EXPECT_EQ(43ul, model->getNumberOfStates());
EXPECT_EQ(59ul, model->getNumberOfTransitions());
ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
size_t initState = 0;
auto labeling = model->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
for (size_t i = 10; i < 43; ++i) {
ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
}
auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[1], true));
EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[2], true));
EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
// Keep labels
auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels);
ASSERT_EQ(13ul, transformed.first->getNumberOfStates());
ASSERT_EQ(29ul, transformed.first->getNumberOfTransitions());
labeling = transformed.first->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
for (size_t i = 5; i < 13; ++i) {
ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
}
EXPECT_EQ(2ul, transformed.second.size());
result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
//result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
//EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
// Merge labels
transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels);
ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions());
labeling = transformed.first->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
for (size_t i = 0; i < 8; ++i) {
ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
}
EXPECT_EQ(2ul, transformed.second.size());
result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
//result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
//EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
// Delete labels
transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels);
ASSERT_EQ(8ul, transformed.first->getNumberOfStates());
ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions());
labeling = transformed.first->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
ASSERT_FALSE(labeling.getStateHasLabel("Fail", 0));
for (size_t i = 1; i < 8; ++i) {
ASSERT_TRUE(labeling.getStateHasLabel("Fail", i));
}
EXPECT_EQ(2ul, transformed.second.size());
result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
//result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
//EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
}
TEST(NonMarkovianChainTransformerTest, ChainElimination2ExampleTest) {
auto model = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination2.drn")->template as<storm::models::sparse::MarkovAutomaton<double>>();
std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]";
auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString));
EXPECT_EQ(10ul, model->getNumberOfStates());
EXPECT_EQ(14ul, model->getNumberOfTransitions());
ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton));
size_t initState = 0;
auto labeling = model->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 7));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 8));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 9));
auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[1], true));
EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formulas[2], true));
EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
// Keep labels
auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels);
ASSERT_EQ(7ul, transformed.first->getNumberOfStates());
ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions());
labeling = transformed.first->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 5));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 6));
EXPECT_EQ(2ul, transformed.second.size());
result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
//result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
//EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
// Merge labels
transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels);
ASSERT_EQ(5ul, transformed.first->getNumberOfStates());
ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
labeling = transformed.first->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2));
ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4));
EXPECT_EQ(2ul, transformed.second.size());
result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
//result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
//EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
// Delete labels
transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels);
ASSERT_EQ(5ul, transformed.first->getNumberOfStates());
ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions());
labeling = transformed.first->getStateLabeling();
ASSERT_TRUE(labeling.getStateHasLabel("init", initState));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1));
ASSERT_FALSE(labeling.getStateHasLabel("Fail", 2));
ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3));
ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4));
EXPECT_EQ(2ul, transformed.second.size());
result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask<double>(transformed.second[0], true));
EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult<double>()[initState]);
result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[1], true));
EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
//result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(transformed.second[2], true));
//EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult<double>()[initState], 1e-6);
}
Loading…
Cancel
Save