Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
InitialConstruct.cpp
Go to the documentation of this file.
1
#include "
storm/storage/prism/InitialConstruct.h
"
2
#include "
storm/storage/expressions/Variable.h
"
3
4
namespace
storm
{
5
namespace
prism {
6
InitialConstruct::InitialConstruct
(
storm::expressions::Expression
initialStatesExpression, std::string
const
& filename, uint_fast64_t lineNumber)
7
:
LocatedInformation
(filename, lineNumber), initialStatesExpression(initialStatesExpression) {
8
// Intentionally left empty.
9
}
10
11
storm::expressions::Expression
InitialConstruct::getInitialStatesExpression
()
const
{
12
return
this->initialStatesExpression;
13
}
14
15
InitialConstruct
InitialConstruct::substitute
(std::map<storm::expressions::Variable, storm::expressions::Expression>
const
& substitution)
const
{
16
return
InitialConstruct
(this->
getInitialStatesExpression
().
substitute
(substitution));
17
}
18
19
std::ostream&
operator<<
(std::ostream& stream,
InitialConstruct
const
& initialConstruct) {
20
stream <<
"init \n"
;
21
stream <<
"\t"
<< initialConstruct.
getInitialStatesExpression
() <<
'\n'
;
22
stream <<
"endinit\n"
;
23
return
stream;
24
}
25
}
// namespace prism
26
}
// namespace storm
InitialConstruct.h
storm::expressions::Expression
Definition
Expression.h:22
storm::prism::InitialConstruct
Definition
InitialConstruct.h:19
storm::prism::InitialConstruct::substitute
InitialConstruct substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all identifiers in the constant according to the given map.
Definition
InitialConstruct.cpp:15
storm::prism::InitialConstruct::InitialConstruct
InitialConstruct()=default
storm::prism::InitialConstruct::getInitialStatesExpression
storm::expressions::Expression getInitialStatesExpression() const
Retrieves the expression characterizing the initial states.
Definition
InitialConstruct.cpp:11
storm::prism::LocatedInformation
Definition
LocatedInformation.h:11
Variable.h
storm::prism::operator<<
std::ostream & operator<<(std::ostream &stream, Assignment const &assignment)
Definition
Assignment.cpp:39
storm
LabParser.cpp.
Definition
cli.cpp:18
src
storm
storage
prism
InitialConstruct.cpp
Generated by
1.9.8