Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
graph.h
Go to the documentation of this file.
1#ifndef STORM_UTILITY_GRAPH_H_
2#define STORM_UTILITY_GRAPH_H_
3
4#include <limits>
5#include <set>
7
12
15
17
18namespace storm {
19namespace storage {
20class BitVector;
21template<typename VT>
22class SparseMatrix;
23} // namespace storage
24
25namespace models {
26
27namespace symbolic {
28template<storm::dd::DdType Type, typename ValueType>
29class Model;
30
31template<storm::dd::DdType Type, typename ValueType>
32class DeterministicModel;
33
34template<storm::dd::DdType Type, typename ValueType>
35class NondeterministicModel;
36
37template<storm::dd::DdType Type, typename ValueType>
38class StochasticTwoPlayerGame;
39} // namespace symbolic
40
41} // namespace models
42
43namespace dd {
44template<storm::dd::DdType Type>
45class Bdd;
46
47template<storm::dd::DdType Type, typename ValueType>
48class Add;
49
50} // namespace dd
51
52namespace storage {
53class ExplicitGameStrategyPair;
54}
55
56namespace utility {
57namespace graph {
58
63template<typename T>
65
80template<typename T>
82 storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates,
83 bool useStepBound = false, uint_fast64_t maximalSteps = 0,
84 boost::optional<storm::storage::BitVector> const& choiceFilter = boost::none);
85
92template<typename T>
94
100template<typename T>
101bool hasCycle(storm::storage::SparseMatrix<T> const& transitionMatrix, boost::optional<storm::storage::BitVector> const& subsystem = boost::none);
102
113template<typename T>
114bool checkIfECWithChoiceExists(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions,
115 storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices);
116
126template<typename T>
127std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates,
128 boost::optional<storm::storage::BitVector> const& subsystem = boost::none);
129
142template<typename T>
144 storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
145
160template<typename T>
162 storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0);
163
176template<typename T>
178 storm::storage::BitVector const& psiStates);
179
190template<typename T>
191std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<T> const& model,
192 storm::storage::BitVector const& phiStates,
193 storm::storage::BitVector const& psiStates);
194
205template<typename T>
206std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<T> const& backwardTransitions,
207 storm::storage::BitVector const& phiStates,
208 storm::storage::BitVector const& psiStates);
209
221template<storm::dd::DdType Type, typename ValueType>
223 storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates,
224 boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
237template<storm::dd::DdType Type, typename ValueType>
239 storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates,
240 storm::dd::Bdd<Type> const& statesWithProbabilityGreater0);
241
252template<storm::dd::DdType Type, typename ValueType>
254 storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
255
265template<storm::dd::DdType Type, typename ValueType>
267 storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
268
279template<storm::dd::DdType Type, typename ValueType>
281 storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
282 storm::dd::Bdd<Type> const& psiStates);
283
293template<typename T, typename SchedulerValueType>
296 boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
297
307template<typename T>
310
324template<typename T, typename SchedulerValueType>
325void computeSchedulerProbGreater0E(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions,
326 storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates,
328 boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
329
338template<typename T, typename SchedulerValueType>
339void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix<T> const& transitionMatrix,
341
349template<typename T, typename SchedulerValueType>
350void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<T> const& transitionMatrix,
352
364template<typename T, typename SchedulerValueType>
365void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<T> const& transitionMatrix,
366 storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
368 boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
369
383template<typename T>
385 storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
386
387template<typename T>
389 storm::storage::BitVector const& psiStates);
390
404template<typename T>
406 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
407 storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
408 storm::storage::BitVector const& psiStates,
409 boost::optional<storm::storage::BitVector> const& choiceConstraint = boost::none);
410
423template<typename T, typename RM>
425 storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
426 storm::storage::BitVector const& psiStates);
427
428template<typename T>
429std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<T> const& transitionMatrix,
430 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
431 storm::storage::SparseMatrix<T> const& backwardTransitions,
432 storm::storage::BitVector const& phiStates,
433 storm::storage::BitVector const& psiStates);
434
445template<typename T, typename RM>
446std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<T, RM> const& model,
447 storm::storage::BitVector const& phiStates,
448 storm::storage::BitVector const& psiStates);
449
465template<typename T>
467 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
468 storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
469 storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0,
470 boost::optional<storm::storage::BitVector> const& choiceConstraint = boost::none);
471
484template<typename T, typename RM>
486 storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
487 storm::storage::BitVector const& psiStates);
488template<typename T>
490 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
491 storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
492 storm::storage::BitVector const& psiStates);
493
506template<typename T, typename RM>
508 storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
509 storm::storage::BitVector const& psiStates);
510
511template<typename T>
513 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
514 storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
515 storm::storage::BitVector const& psiStates);
516
517template<typename T>
518std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<T> const& transitionMatrix,
519 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
520 storm::storage::SparseMatrix<T> const& backwardTransitions,
521 storm::storage::BitVector const& phiStates,
522 storm::storage::BitVector const& psiStates);
523
534template<typename T, typename RM>
535std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<T, RM> const& model,
536 storm::storage::BitVector const& phiStates,
537 storm::storage::BitVector const& psiStates);
538
549template<storm::dd::DdType Type, typename ValueType = double>
551 storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
552 storm::dd::Bdd<Type> const& psiStates);
553
557template<storm::dd::DdType Type, typename ValueType>
559 storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
560 storm::dd::Bdd<Type> const& psiStates);
561
572template<storm::dd::DdType Type, typename ValueType = double>
574 storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
575
586template<storm::dd::DdType Type, typename ValueType = double>
588 storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
589 storm::dd::Bdd<Type> const& psiStates);
590
601template<storm::dd::DdType Type, typename ValueType = double>
603 storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
604
616template<storm::dd::DdType Type, typename ValueType = double>
618 storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0A);
619
632template<storm::dd::DdType Type, typename ValueType = double>
634 storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates,
635 storm::dd::Bdd<Type> const& statesWithProbabilityGreater0E);
636
640template<storm::dd::DdType Type, typename ValueType>
642 storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
643 storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbability1E);
644
645template<storm::dd::DdType Type, typename ValueType = double>
647 storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
648
649template<storm::dd::DdType Type, typename ValueType = double>
651 storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
652 storm::dd::Bdd<Type> const& psiStates);
653
654template<storm::dd::DdType Type, typename ValueType = double>
656 storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
657
658template<storm::dd::DdType Type, typename ValueType = double>
660 storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
661 storm::dd::Bdd<Type> const& psiStates);
662
663template<storm::dd::DdType Type>
672
673 bool hasPlayer1Strategy() const {
674 return static_cast<bool>(player1Strategy);
675 }
676
678 return player1Strategy.get();
679 }
680
681 boost::optional<storm::dd::Bdd<Type>> const& getOptionalPlayer1Strategy() {
682 return player1Strategy;
683 }
684
685 bool hasPlayer2Strategy() const {
686 return static_cast<bool>(player2Strategy);
687 }
688
690 return player2Strategy.get();
691 }
692
693 boost::optional<storm::dd::Bdd<Type>> const& getOptionalPlayer2Strategy() {
694 return player2Strategy;
695 }
696
698 return player1States;
699 }
700
702 return player2States;
703 }
704
707 boost::optional<storm::dd::Bdd<Type>> player1Strategy;
708 boost::optional<storm::dd::Bdd<Type>> player2Strategy;
709};
710
721template<storm::dd::DdType Type, typename ValueType>
723 storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
724 storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy,
725 storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false,
726 bool producePlayer2Strategy = false);
727
739template<storm::dd::DdType Type, typename ValueType>
741 storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
742 storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy,
743 storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false,
744 bool producePlayer2Strategy = false, boost::optional<storm::dd::Bdd<Type>> const& player1Candidates = boost::none);
745
748 ExplicitGameProb01Result(uint64_t numberOfPlayer1States, uint64_t numberOfPlayer2States)
749 : player1States(numberOfPlayer1States), player2States(numberOfPlayer2States) {
750 // Intentionally left empty.
751 }
752
757
759 return player1States;
760 }
761
763 return player2States;
764 }
765
768};
769
784template<typename ValueType>
785ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups,
786 storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions,
787 std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates,
788 storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction,
789 storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair = nullptr);
790
806template<typename ValueType>
807ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups,
808 storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions,
809 std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates,
810 storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction,
811 storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair = nullptr,
812 boost::optional<storm::storage::BitVector> const& player1Candidates = boost::none);
813
820template<typename T>
821std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix, std::vector<uint64_t> const& firstStates = {});
822
823template<typename T>
824std::vector<uint_fast64_t> getBFSSort(storm::storage::SparseMatrix<T> const& matrix, std::vector<uint_fast64_t> const& firstStates);
825
826} // namespace graph
827} // namespace utility
828} // namespace storm
829
830#endif /* STORM_UTILITY_GRAPH_H_ */
The base class of all sparse deterministic models.
The base class of sparse nondeterministic models.
Base class for all deterministic symbolic models.
Base class for all symbolic models.
Definition Model.h:45
Base class for all nondeterministic symbolic models.
This class represents a discrete-time stochastic two-player game.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
This class defines which action is chosen in a particular state of a non-deterministic model.
Definition Scheduler.h:18
A class that holds a possibly non-square matrix in the compressed row storage format.
SFTBDDChecker::Bdd Bdd
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01(storm::models::sparse::DeterministicModel< T > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi i...
Definition graph.cpp:399
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01Max(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Definition graph.cpp:825
void computeSchedulerStayingInStates(storm::storage::BitVector const &states, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
Computes a scheduler for the given states that chooses an action that stays completely in the very sa...
Definition graph.cpp:489
ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Groups, storm::storage::SparseMatrix< ValueType > const &player1BackwardTransitions, std::vector< uint64_t > const &player2BackwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::storage::ExplicitGameStrategyPair *strategyPair)
Computes the set of states that have probability 0 given the strategies of the two players.
Definition graph.cpp:1298
std::vector< uint_fast64_t > getTopologicalSort(storm::storage::SparseMatrix< T > const &matrix, std::vector< uint64_t > const &firstStates)
Performs a topological sort of the states of the system according to the given transitions.
Definition graph.cpp:1851
void computeSchedulerProbGreater0E(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
Computes a scheduler for the ProbGreater0E-States such that in the induced system the given psiStates...
Definition graph.cpp:541
std::vector< uint_fast64_t > getBFSSort(storm::storage::SparseMatrix< T > const &matrix, std::vector< uint_fast64_t > const &firstStates)
Definition graph.cpp:1817
storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &constraintStates, storm::storage::BitVector const &targetStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional< storm::storage::BitVector > const &choiceFilter)
Performs a forward depth-first search through the underlying graph structure to identify the states t...
Definition graph.cpp:47
storm::storage::BitVector getReachableOneStep(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates)
Computes the states reachable in one step from the states indicated by the bitvector.
Definition graph.cpp:35
storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps)
Performs a backward depth-first search trough the underlying graph structure of the given model to de...
Definition graph.cpp:321
void computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const &states, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler)
Definition graph.cpp:514
storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional< storm::storage::BitVector > const &choiceConstraint)
Computes the sets of states that have probability greater 0 of satisfying phi until psi under any pos...
Definition graph.cpp:847
void computeSchedulerProb1E(storm::storage::BitVector const &prob1EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
Computes a scheduler for the given prob1EStates such that in the induced system the given psiStates a...
Definition graph.cpp:614
bool hasCycle(storm::storage::SparseMatrix< T > const &transitionMatrix, boost::optional< storm::storage::BitVector > const &subsystem)
Returns true if the graph represented by the given matrix has a cycle.
Definition graph.cpp:142
storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 1 of satisfying phi until psi under all possible re...
Definition graph.cpp:987
storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps)
Computes the sets of states that have probability greater 0 of satisfying phi until psi under at leas...
Definition graph.cpp:679
storm::storage::BitVector performProb0A(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Definition graph.cpp:739
storm::storage::BitVector performProb1(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &, storm::storage::BitVector const &psiStates, storm::storage::BitVector const &statesWithProbabilityGreater0)
Computes the set of states of the given model for which all paths lead to the given set of target sta...
Definition graph.cpp:382
bool checkIfECWithChoiceExists(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &subsystem, storm::storage::BitVector const &choices)
Checks whether there is an End Component that.
Definition graph.cpp:181
storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 0 of satisfying phi until psi under at least one po...
Definition graph.cpp:966
storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix< T > const &transitionMatrix)
Retrieves a set of states that covers als BSCCs of the system in the sense that for every BSCC exactl...
Definition graph.cpp:128
void computeSchedulerProb0E(storm::storage::BitVector const &prob0EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler)
Computes a scheduler for the given states that have a scheduler that has a probability 0.
Definition graph.cpp:592
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01Min(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Definition graph.cpp:1069
std::vector< uint_fast64_t > getDistances(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, boost::optional< storm::storage::BitVector > const &subsystem)
Performs a breadth-first search through the underlying graph structure to compute the distance from a...
Definition graph.cpp:287
storm::storage::BitVector performProb1E(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, boost::optional< storm::storage::BitVector > const &choiceConstraint)
Computes the sets of states that have probability 1 of satisfying phi until psi under at least one po...
Definition graph.cpp:747
void computeSchedulerRewInf(storm::storage::BitVector const &rewInfStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::Scheduler< SchedulerValueType > &scheduler)
Computes a scheduler for the given states that have a scheduler that has a reward infinity.
Definition graph.cpp:598
storage::BitVector BitVector
LabParser.cpp.
ExplicitGameProb01Result(storm::storage::BitVector const &player1States, storm::storage::BitVector const &player2States)
Definition graph.h:753
storm::storage::BitVector const & getPlayer1States() const
Definition graph.h:758
storm::storage::BitVector player2States
Definition graph.h:767
storm::storage::BitVector const & getPlayer2States() const
Definition graph.h:762
ExplicitGameProb01Result(uint64_t numberOfPlayer1States, uint64_t numberOfPlayer2States)
Definition graph.h:748
storm::storage::BitVector player1States
Definition graph.h:766
boost::optional< storm::dd::Bdd< Type > > player1Strategy
Definition graph.h:707
SymbolicGameProb01Result(storm::dd::Bdd< Type > const &player1States, storm::dd::Bdd< Type > const &player2States, boost::optional< storm::dd::Bdd< Type > > const &player1Strategy=boost::none, boost::optional< storm::dd::Bdd< Type > > const &player2Strategy=boost::none)
Definition graph.h:666
boost::optional< storm::dd::Bdd< Type > > const & getOptionalPlayer2Strategy()
Definition graph.h:693
storm::dd::Bdd< Type > const & getPlayer2States() const
Definition graph.h:701
storm::dd::Bdd< Type > const & getPlayer1Strategy() const
Definition graph.h:677
boost::optional< storm::dd::Bdd< Type > > const & getOptionalPlayer1Strategy()
Definition graph.h:681
storm::dd::Bdd< Type > const & getPlayer2Strategy() const
Definition graph.h:689
boost::optional< storm::dd::Bdd< Type > > player2Strategy
Definition graph.h:708
storm::dd::Bdd< Type > const & getPlayer1States() const
Definition graph.h:697