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

Merge branch 'master' into parametricSystems 

Former-commit-id: fda6a085e6
tempestpy_adaptions
dehnert 10 years ago
parent
19bc5eb995 2dae5862c8
commit
a41a2d166e
2 changed files with 9 additions and 11 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. 8
      src/storage/DeterministicModelBisimulationDecomposition.cpp
  2. 12
      src/storage/DeterministicModelBisimulationDecomposition.h

8
src/storage/DeterministicModelBisimulationDecomposition.cpp
View File

@ -616,7 +616,7 @@ namespace storm {
}
for (auto const& expressionFormula : atomicExpressionFormulas) {
std::stringstream stream;
stream << expressionFormula;
stream << *expressionFormula;
labelsToRespect.insert(stream.str());
}
respectedAtomicPropositions = labelsToRespect;
@ -723,7 +723,7 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) {
void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, std::set<std::string> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) {
// In order to create the quotient model, we need to construct
// (a) the new transition matrix,
// (b) the new labeling,
@ -734,7 +734,7 @@ namespace storm {
// Prepare the new state labeling for (b).
storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
std::set<std::string> atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions();
std::set<std::string> atomicPropositionsSet = selectedAtomicPropositions;
atomicPropositionsSet.insert("init");
std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
for (auto const& ap : atomicPropositions) {
@ -840,7 +840,7 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) {
void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, std::set<std::string> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue.

12
src/storage/DeterministicModelBisimulationDecomposition.h
View File

@ -413,8 +413,7 @@ namespace storm {
* getQuotient().
*
* @param model The model on whose state space to compute the coarses strong bisimulation relation.
* @param atomicPropositions The set of atomic propositions that the bisimulation considers. If not given,
* all atomic propositions are considered.
* @param atomicPropositions The set of atomic propositions that the bisimulation considers.
* @param backwardTransitions The backward transitions of the model.
* @param The initial partition.
* @param bisimulationType The kind of bisimulation that is to be computed.
@ -422,7 +421,7 @@ namespace storm {
* method.
*/
template<typename ModelType>
void partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient);
void partitionRefinement(ModelType const& model, std::set<std::string> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient);
/*!
* Refines the partition based on the provided splitter. After calling this method all blocks are stable
@ -466,15 +465,14 @@ namespace storm {
*
* @param model The model whose state space was used for computing the equivalence classes. This is used for
* determining the transitions of each equivalence class.
* @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. The
* quotient will only have these atomic propositions. If not given, all atomic propositions will be
* considered.
* @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation.
* The quotient will only have these atomic propositions.
* @param partition The previously computed partition. This is used for quickly retrieving the block of a
* state.
* @param bisimulationType The kind of bisimulation that is to be computed.
*/
template<typename ModelType>
void buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards);
void buildQuotient(ModelType const& model, std::set<std::string> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards);
/*!
* Creates the measure-driven initial partition for reaching psi states from phi states.

Write Preview
Loading…
Cancel
Save