RegionConstraintChecker.h File Reference

#include <map>
#include <optional>
#include <ostream>
#include <string>
#include <vector>
#include "storm-pars/storage/ParameterRegion.h"
#include "storm/analysis/GraphConditions.h"
#include "storm/solver/SmtSolver.h"
#include "storm/storage/expressions/Expression.h"

Include dependency graph for RegionConstraintChecker.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	storm::pars::analysis::RegionWitness
	A point of a parameter region, mapping the variables to exact values. More...
struct	storm::pars::analysis::RegionCheckResult
class	storm::pars::analysis::RegionConstraintChecker
	Checks whether the constraints collected for a parametric model hold over an entire rectangular region. More...

Namespaces
namespace	storm
namespace	storm::pars
namespace	storm::pars::analysis

Typedefs
using	storm::pars::analysis::RationalFunctionRegion = storm::storage::ParameterRegion<storm::RationalFunction>
using	storm::pars::analysis::CoefficientType = RationalFunctionRegion::CoefficientType
using	storm::pars::analysis::ConstraintVerdict = storm::solver::SmtSolver::CheckResult
	Tri-state outcome of a check: Sat means the constraint holds on the whole region, Unsat means it is violated somewhere (a witness is available), and Unknown means neither could be established.

Functions
std::ostream &	storm::pars::analysis::operator<< (std::ostream &out, RegionWitness const &witness)
	Prints the witness as a comma-separated list of assignments, e.g.