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

Added the possibility to build the bisimulation options from a formula in the sense that it automatically picks suitable settings for the formula. 

Former-commit-id: 932c7d899a
tempestpy_adaptions
dehnert 10 years ago
parent
4952306092
commit
ed4f1bb7cf
3 changed files with 112 additions and 26 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. 65
      src/storage/DeterministicModelBisimulationDecomposition.cpp
  2. 32
      src/storage/DeterministicModelBisimulationDecomposition.h
  3. 41
      test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp

65
src/storage/DeterministicModelBisimulationDecomposition.cpp
View File

@ -194,6 +194,22 @@ namespace storm {
return this->absorbing;
}
template<typename ValueType>
void DeterministicModelBisimulationDecomposition<ValueType>::Block::setRepresentativeState(storm::storage::sparse::state_type representativeState) {
this->representativeState = representativeState;
}
template<typename ValueType>
bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasRepresentativeState() const {
return static_cast<bool>(representativeState);
}
template<typename ValueType>
storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getRepresentativeState() const {
STORM_LOG_THROW(representativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block.");
return representativeState.get();
}
template<typename ValueType>
storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
return this->markedPosition;
@ -249,7 +265,7 @@ namespace storm {
}
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional<storm::storage::sparse::state_type> representativeProb1State, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
storm::storage::sparse::state_type position = 0;
Block* firstBlock = nullptr;
Block* secondBlock = nullptr;
@ -280,6 +296,7 @@ namespace storm {
++position;
}
secondBlock->setAbsorbing(true);
secondBlock->setRepresentativeState(representativeProb1State.get());
}
storm::storage::BitVector otherStates = ~(prob0States | prob1States);
@ -577,7 +594,7 @@ namespace storm {
}
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::logic::Formula const& formula) : Options() {
DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::models::AbstractModel<ValueType> const& model, storm::logic::Formula const& formula) : Options() {
if (!formula.containsRewardOperator()) {
this->keepRewards = false;
}
@ -632,13 +649,16 @@ namespace storm {
}
if (measureDrivenInitialPartition) {
phiStateFormula = leftSubformula;
psiStateFormula = rightSubformula;
storm::modelchecker::SparsePropositionalModelChecker<ValueType> checker(model);
std::unique_ptr<storm::modelchecker::CheckResult> phiStatesCheckResult = checker.check(*leftSubformula);
std::unique_ptr<storm::modelchecker::CheckResult> psiStatesCheckResult = checker.check(*rightSubformula);
phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
}
}
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStateFormula(), psiStateFormula(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
// Intentionally left empty.
}
@ -658,9 +678,9 @@ namespace storm {
Partition initialPartition;
if (options.measureDrivenInitialPartition) {
STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded);
STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded);
} else {
initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards);
}
@ -684,9 +704,9 @@ namespace storm {
Partition initialPartition;
if (options.measureDrivenInitialPartition) {
STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded);
STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states.");
initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded);
} else {
initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards);
}
@ -751,8 +771,13 @@ namespace storm {
if (oldBlock.isAbsorbing()) {
builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne<ValueType>());
// Otherwise add all atomic propositions to the equivalence class that the representative state
// satisfies.
// If the block has a special representative state, we retrieve it now.
if (oldBlock.hasRepresentativeState()) {
representativeState = oldBlock.getRepresentativeState();
}
// Add all of the selected atomic propositions that hold in the representative state to the state
// representing the block.
for (auto const& ap : atomicPropositions) {
if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
newLabeling.addAtomicPropositionToState(ap, blockIndex);
@ -1264,13 +1289,15 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::shared_ptr<storm::logic::Formula const> const& phiStateFormula, std::shared_ptr<storm::logic::Formula const> const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards, bool bounded) {
storm::modelchecker::SparsePropositionalModelChecker<ValueType> checker(model);
std::unique_ptr<storm::modelchecker::CheckResult> phiStates = checker.check(*phiStateFormula);
std::unique_ptr<storm::modelchecker::CheckResult> psiStates = checker.check(*psiStateFormula);
typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards, bool bounded) {
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates);
boost::optional<storm::storage::sparse::state_type> representativePsiState;
if (!psiStates.empty()) {
representativePsiState = *psiStates.begin();
}
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates->asExplicitQualitativeCheckResult().getTruthValuesVector(), psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector());
Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector() : statesWithProbability01.second, bisimulationType == BisimulationType::WeakDtmc);
Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates : statesWithProbability01.second, representativePsiState, bisimulationType == BisimulationType::WeakDtmc);
// If the model has state rewards, we need to consider them, because otherwise reward properties are not
// preserved.

32
src/storage/DeterministicModelBisimulationDecomposition.h
View File

@ -31,16 +31,18 @@ namespace storm {
* Creates an object representing the options necessary to obtain the smallest quotient while still
* preserving the given formula.
*
* @param The model for which the quotient model shall be computed. This needs to be given in order to
* derive a suitable initial partition.
* @param formula The formula that is to be preserved.
*/
Options(storm::logic::Formula const& formula);
Options(storm::models::AbstractModel<ValueType> const& model, storm::logic::Formula const& formula);
// A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
// to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
// measure driven initial partition wrt. to the states phi and psi is taken.
bool measureDrivenInitialPartition;
boost::optional<std::shared_ptr<storm::logic::Formula const>> phiStateFormula;
boost::optional<std::shared_ptr<storm::logic::Formula const>> psiStateFormula;
boost::optional<storm::storage::BitVector> phiStates;
boost::optional<storm::storage::BitVector> psiStates;
// An optional set of strings that indicate which of the atomic propositions of the model are to be
// respected and which may be ignored. If not given, all atomic propositions of the model are respected.
@ -201,6 +203,15 @@ namespace storm {
// Retrieves whether the block is to be interpreted as absorbing.
bool isAbsorbing() const;
// Sets the representative state of this block
void setRepresentativeState(storm::storage::sparse::state_type representativeState);
// Retrieves the representative state for this block.
bool hasRepresentativeState() const;
// Retrieves the representative state for this block.
storm::storage::sparse::state_type getRepresentativeState() const;
private:
// An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
// kept by the partition.
@ -228,6 +239,10 @@ namespace storm {
// The ID of the block. This is only used for debugging purposes.
std::size_t id;
// An optional representative state for the block. If this is set, this state is used to derive the
// atomic propositions of the meta state in the quotient model.
boost::optional<storm::storage::sparse::state_type> representativeState;
};
class Partition {
@ -250,9 +265,12 @@ namespace storm {
* @param numberOfStates The number of states the partition holds.
* @param prob0States The states which have probability 0 of satisfying phi until psi.
* @param prob1States The states which have probability 1 of satisfying phi until psi.
* @param representativeProb1State If the set of prob1States is non-empty, this needs to be a state
* that is representative for this block in the sense that the state representing this block in the quotient
* model will receive exactly the atomic propositions of the representative state.
* @param keepSilentProbabilities A flag indicating whether or not silent probabilities are to be tracked.
*/
Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities = false);
Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional<storm::storage::sparse::state_type> representativeProb1State, bool keepSilentProbabilities = false);
Partition() = default;
Partition(Partition const& other) = default;
@ -464,15 +482,15 @@ namespace storm {
* @param model The model whose state space is partitioned based on reachability of psi states from phi
* states.
* @param backwardTransitions The backward transitions of the model.
* @param phiStateFormula The formula that defines the phi states in the model.
* @param psiStateFormula The formula that defines the psi states in the model.
* @param phiStates The phi states in the model.
* @param psiStates The psi states in the model.
* @param bisimulationType The kind of bisimulation that is to be computed.
* @param bounded If set to true, the initial partition will be chosen in such a way that preserves bounded
* reachability queries.
* @return The resulting partition.
*/
template<typename ModelType>
Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::shared_ptr<storm::logic::Formula const> const& phiStateFormula, std::shared_ptr<storm::logic::Formula const> const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false);
Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false);
/*!
* Creates the initial partition based on all the labels in the given model.

41
test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
View File

@ -36,6 +36,16 @@ TEST(DeterministicModelBisimulationDecomposition, Die) {
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(5, result->getNumberOfStates());
EXPECT_EQ(8, result->getNumberOfTransitions());
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim4(*dtmc, options2);
ASSERT_NO_THROW(result = bisim4.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(5, result->getNumberOfStates());
EXPECT_EQ(8, result->getNumberOfTransitions());
}
TEST(DeterministicModelBisimulationDecomposition, Crowds) {
@ -71,4 +81,35 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(43, result->getNumberOfStates());
EXPECT_EQ(83, result->getNumberOfTransitions());
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options2(*dtmc, *eventuallyFormula);
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim4(*dtmc, options2);
ASSERT_NO_THROW(result = bisim4.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(64, result->getNumberOfStates());
EXPECT_EQ(104, result->getNumberOfTransitions());
auto probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(eventuallyFormula);
typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options3(*dtmc, *probabilityOperatorFormula);
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim5(*dtmc, options3);
ASSERT_NO_THROW(result = bisim5.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(64, result->getNumberOfStates());
EXPECT_EQ(104, result->getNumberOfTransitions());
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), labelFormula, 50);
typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options4(*dtmc, *boundedUntilFormula);
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim6(*dtmc, options4);
ASSERT_NO_THROW(result = bisim6.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(65, result->getNumberOfStates());
EXPECT_EQ(105, result->getNumberOfTransitions());
}
Write Preview
Loading…
Cancel
Save