#include "storm-config.h"#include "test/storm_gtest.h"#include <memory>#include <string>#include "storm-pars/analysis/RegionConstraintChecker.h"#include "storm-parsers/api/storm-parsers.h"#include "storm/adapters/RationalFunctionAdapter.h"#include "storm/analysis/GraphConditions.h"#include "storm/api/properties.h"#include "storm/builder/ExplicitModelBuilder.h"#include "storm/exceptions/InvalidArgumentException.h"#include "storm/generator/NextStateGenerator.h"#include "storm/models/sparse/Dtmc.h"#include "storm/storage/expressions/ExpressionManager.h"#include "storm/storage/jani/Property.h"#include "storm/utility/constants.h"
Go to the source code of this file.
Functions | |
| TEST (RegionConstraintCheckerTest, AffineConstraintHoldsThroughout) | |
| TEST (RegionConstraintCheckerTest, AffineConstraintViolatedAtCorner) | |
| TEST (RegionConstraintCheckerTest, StrictInequalityOnBoundaryIsViolated) | |
| TEST (RegionConstraintCheckerTest, NegativeCoefficientIsHandled) | |
| TEST (RegionConstraintCheckerTest, NotEqualOverPositiveRegion) | |
| TEST (RegionConstraintCheckerTest, EqualityRequiresIdenticallyZero) | |
| TEST (RegionConstraintCheckerTest, BooleanLiteralConstraintsAreDecided) | |
| TEST (RegionConstraintCheckerTest, CancellingCoefficientDoesNotRequireVariableInRegion) | |
| TEST (RegionConstraintCheckerTest, NonLinearConstraintIsUndecided) | |
| TEST (RegionConstraintCheckerTest, IfThenElseIsUndecided) | |
| TEST (RegionConstraintCheckerTest, MissingVariableIsRejected) | |
| TEST (RegionConstraintCheckerTest, RealModelConstraintsAreDecidedExactly) | |
| TEST (RegionConstraintCheckerTest, NonAffineModelConstraintsAreNeverClaimedToHold) | |
Function Documentation
◆ TEST() [1/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| AffineConstraintHoldsThroughout | ) |
Definition at line 75 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [2/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| AffineConstraintViolatedAtCorner | ) |
Definition at line 91 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [3/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| BooleanLiteralConstraintsAreDecided | ) |
Definition at line 177 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [4/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| CancellingCoefficientDoesNotRequireVariableInRegion | ) |
Definition at line 194 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [5/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| EqualityRequiresIdenticallyZero | ) |
Definition at line 161 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [6/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| IfThenElseIsUndecided | ) |
Definition at line 216 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [7/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| MissingVariableIsRejected | ) |
Definition at line 229 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [8/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| NegativeCoefficientIsHandled | ) |
Definition at line 126 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [9/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| NonAffineModelConstraintsAreNeverClaimedToHold | ) |
Definition at line 292 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [10/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| NonLinearConstraintIsUndecided | ) |
Definition at line 203 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [11/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| NotEqualOverPositiveRegion | ) |
Definition at line 146 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [12/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| RealModelConstraintsAreDecidedExactly | ) |
Definition at line 239 of file RegionConstraintCheckerTest.cpp.
◆ TEST() [13/13]
| TEST | ( | RegionConstraintCheckerTest | , |
| StrictInequalityOnBoundaryIsViolated | ) |
Definition at line 108 of file RegionConstraintCheckerTest.cpp.
