#include <JaniLocalEliminator.h>

Public Member Functions
	Session (Model model, Property property, bool flatten=true)
Model &	getModel ()
void	setModel (const Model &model)
Property &	getProperty ()
bool	getFinished () const
void	setFinished (bool finished)
AutomatonInfo &	getAutomatonInfo (const std::string &name)
void	buildAutomataInfo ()
void	flatten_automata ()
void	addMissingGuards (const std::string &automatonName)
expressions::Expression	getNewGuard (const Edge &edge, const EdgeDestination &dest, const Edge &outgoing)
expressions::Expression	getProbability (const EdgeDestination &first, const EdgeDestination &then)
OrderedAssignments	executeInSequence (const EdgeDestination &first, const EdgeDestination &then, std::set< std::string > &rewardVariables)
bool	isEliminable (const std::string &automatonName, std::string const &locationName)
bool	hasLoops (const std::string &automatonName, std::string const &locationName)
bool	hasNamedActions (const std::string &automatonName, std::string const &locationName)
bool	isPossiblyInitial (const std::string &automatonName, std::string const &locationName)
bool	isPartOfProp (const std::string &automatonName, std::string const &locationName)
bool	isPartOfProp (const std::string &automatonName, uint64_t locationIndex)
bool	computeIsPartOfProp (const std::string &automatonName, const std::string &locationName)
bool	computeIsPartOfProp (const std::string &automatonName, uint64_t locationIndex)
bool	computeIsPartOfProp (const std::map< expressions::Variable, expressions::Expression > &substitutionMap)
void	setPartOfProp (const std::string &automatonName, const std::string &locationName, bool isPartOfProp)
void	setPartOfProp (const std::string &automatonName, uint64_t locationIndex, bool isPartOfProp)
void	clearIsPartOfProp (const std::string &automatonName)
bool	isVariablePartOfProperty (const std::string &expressionVariableName)

Public Attributes
bool	isRewardFormula
std::set< std::string >	rewardModels

Detailed Description

Definition at line 30 of file JaniLocalEliminator.h.

Constructor & Destructor Documentation

◆ Session()

storm::jani::JaniLocalEliminator::Session::Session	(	Model	model,
		Property	property,
		bool	flatten = true )

explicit

Definition at line 262 of file JaniLocalEliminator.cpp.

Member Function Documentation

◆ addMissingGuards()

void storm::jani::JaniLocalEliminator::Session::addMissingGuards ( const std::string & automatonName )

Definition at line 366 of file JaniLocalEliminator.cpp.

◆ buildAutomataInfo()

void storm::jani::JaniLocalEliminator::Session::buildAutomataInfo ( )

Definition at line 445 of file JaniLocalEliminator.cpp.

◆ clearIsPartOfProp()

void storm::jani::JaniLocalEliminator::Session::clearIsPartOfProp ( const std::string & automatonName )

Definition at line 210 of file JaniLocalEliminator.cpp.

◆ computeIsPartOfProp() [1/3]

bool storm::jani::JaniLocalEliminator::Session::computeIsPartOfProp ( const std::map< expressions::Variable, expressions::Expression > & substitutionMap )

Definition at line 163 of file JaniLocalEliminator.cpp.

◆ computeIsPartOfProp() [2/3]

bool storm::jani::JaniLocalEliminator::Session::computeIsPartOfProp	(	const std::string &	automatonName,
		const std::string &	locationName )

Definition at line 145 of file JaniLocalEliminator.cpp.

◆ computeIsPartOfProp() [3/3]

bool storm::jani::JaniLocalEliminator::Session::computeIsPartOfProp	(	const std::string &	automatonName,
		uint64_t	locationIndex )

Definition at line 151 of file JaniLocalEliminator.cpp.

◆ executeInSequence()

OrderedAssignments storm::jani::JaniLocalEliminator::Session::executeInSequence	(	const EdgeDestination &	first,
		const EdgeDestination &	then,
		std::set< std::string > &	rewardVariables )

Definition at line 312 of file JaniLocalEliminator.cpp.

◆ flatten_automata()

void storm::jani::JaniLocalEliminator::Session::flatten_automata ( )

Definition at line 360 of file JaniLocalEliminator.cpp.

◆ getAutomatonInfo()

JaniLocalEliminator::AutomatonInfo & storm::jani::JaniLocalEliminator::Session::getAutomatonInfo ( const std::string & name )

Definition at line 455 of file JaniLocalEliminator.cpp.

◆ getFinished()

bool storm::jani::JaniLocalEliminator::Session::getFinished ( ) const

Definition at line 295 of file JaniLocalEliminator.cpp.

◆ getModel()

Model & storm::jani::JaniLocalEliminator::Session::getModel ( )

Definition at line 283 of file JaniLocalEliminator.cpp.

◆ getNewGuard()

expressions::Expression storm::jani::JaniLocalEliminator::Session::getNewGuard	(	const Edge &	edge,
		const EdgeDestination &	dest,
		const Edge &	outgoing )

Definition at line 303 of file JaniLocalEliminator.cpp.

◆ getProbability()

expressions::Expression storm::jani::JaniLocalEliminator::Session::getProbability	(	const EdgeDestination &	first,
		const EdgeDestination &	then )

Definition at line 308 of file JaniLocalEliminator.cpp.

◆ getProperty()

Property & storm::jani::JaniLocalEliminator::Session::getProperty ( )

Definition at line 291 of file JaniLocalEliminator.cpp.

◆ hasLoops()

bool storm::jani::JaniLocalEliminator::Session::hasLoops	(	const std::string &	automatonName,
		std::string const &	locationName )

Definition at line 80 of file JaniLocalEliminator.cpp.

◆ hasNamedActions()

bool storm::jani::JaniLocalEliminator::Session::hasNamedActions	(	const std::string &	automatonName,
		std::string const &	locationName )

Definition at line 91 of file JaniLocalEliminator.cpp.

◆ isEliminable()

bool storm::jani::JaniLocalEliminator::Session::isEliminable	(	const std::string &	automatonName,
		std::string const &	locationName )

Definition at line 77 of file JaniLocalEliminator.cpp.

◆ isPartOfProp() [1/2]

bool storm::jani::JaniLocalEliminator::Session::isPartOfProp	(	const std::string &	automatonName,
		std::string const &	locationName )

Definition at line 135 of file JaniLocalEliminator.cpp.

◆ isPartOfProp() [2/2]

bool storm::jani::JaniLocalEliminator::Session::isPartOfProp	(	const std::string &	automatonName,
		uint64_t	locationIndex )

Definition at line 140 of file JaniLocalEliminator.cpp.

◆ isPossiblyInitial()

bool storm::jani::JaniLocalEliminator::Session::isPossiblyInitial	(	const std::string &	automatonName,
		std::string const &	locationName )

Definition at line 102 of file JaniLocalEliminator.cpp.

◆ isVariablePartOfProperty()

bool storm::jani::JaniLocalEliminator::Session::isVariablePartOfProperty ( const std::string & expressionVariableName )

Definition at line 354 of file JaniLocalEliminator.cpp.

◆ setFinished()

void storm::jani::JaniLocalEliminator::Session::setFinished ( bool finished )

Definition at line 299 of file JaniLocalEliminator.cpp.

◆ setModel()

void storm::jani::JaniLocalEliminator::Session::setModel ( const Model & model )

Definition at line 287 of file JaniLocalEliminator.cpp.

◆ setPartOfProp() [1/2]

void storm::jani::JaniLocalEliminator::Session::setPartOfProp	(	const std::string &	automatonName,
		const std::string &	locationName,
		bool	isPartOfProp )

Definition at line 192 of file JaniLocalEliminator.cpp.

◆ setPartOfProp() [2/2]

void storm::jani::JaniLocalEliminator::Session::setPartOfProp	(	const std::string &	automatonName,
		uint64_t	locationIndex,
		bool	isPartOfProp )

Definition at line 197 of file JaniLocalEliminator.cpp.

Member Data Documentation

◆ isRewardFormula

bool storm::jani::JaniLocalEliminator::Session::isRewardFormula

Definition at line 61 of file JaniLocalEliminator.h.

◆ rewardModels

std::set<std::string> storm::jani::JaniLocalEliminator::Session::rewardModels

Definition at line 62 of file JaniLocalEliminator.h.

The documentation for this class was generated from the following files:

src/storm/storage/jani/localeliminator/JaniLocalEliminator.h
src/storm/storage/jani/localeliminator/JaniLocalEliminator.cpp

Public Member Functions

Public Attributes