Browse Source
Update src/storm/storage/prism/OverlappingGuardAnalyser.h
Co-authored-by: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
tempestpy_adaptions
Sebastian Junges
4 years ago
committed by
GitHub
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with
7 additions and
1 deletions
-
src/storm/storage/prism/OverlappingGuardAnalyser.h
|
|
@ -20,8 +20,15 @@ namespace storm { |
|
|
class OverlappingGuardAnalyser { |
|
|
class OverlappingGuardAnalyser { |
|
|
public: |
|
|
public: |
|
|
OverlappingGuardAnalyser(Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory>& smtSolverFactory); |
|
|
OverlappingGuardAnalyser(Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory>& smtSolverFactory); |
|
|
|
|
|
/*! |
|
|
|
|
|
* returns true iff there are two commands that |
|
|
|
|
|
* * are contained in the same module, |
|
|
|
|
|
* * either have the same action label or are both unlabeled, and |
|
|
|
|
|
* * have overlapping guards, i.e., can be enabled simultaneously. |
|
|
|
|
|
*/ |
|
|
bool hasModuleWithInnerActionOverlap(); |
|
|
bool hasModuleWithInnerActionOverlap(); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
private: |
|
|
private: |
|
|
Program const& program; |
|
|
Program const& program; |
|
|
std::unique_ptr<storm::solver::SmtSolver> smtSolver; |
|
|
std::unique_ptr<storm::solver::SmtSolver> smtSolver; |
|
|
@ -29,4 +36,3 @@ namespace storm { |
|
|
}; |
|
|
}; |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
|
