Browse Source

Added proper canHandle method to propositional model checker.

Former-commit-id: 4af714e31a
tempestpy_adaptions
dehnert 10 years ago
parent
commit
cc7d44dd15
  1. 5
      src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
  2. 1
      src/modelchecker/propositional/SparsePropositionalModelChecker.h

5
src/modelchecker/propositional/SparsePropositionalModelChecker.cpp

@ -15,6 +15,11 @@ namespace storm {
// Intentionally left empty.
}
template<typename ValueType>
bool SparsePropositionalModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const {
return formula.isPropositionalFormula();
}
template<typename ValueType>
std::unique_ptr<CheckResult> SparsePropositionalModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
if (stateFormula.isTrueFormula()) {

1
src/modelchecker/propositional/SparsePropositionalModelChecker.h

@ -14,6 +14,7 @@ namespace storm {
explicit SparsePropositionalModelChecker(storm::models::AbstractModel<ValueType> const& model);
// The implemented methods of the AbstractModelChecker interface.
virtual bool canHandle(storm::logic::Formula const& formula) const override;
virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;

Loading…
Cancel
Save