Browse Source
(LTL) ExtractMaximalStateFormulasVisitor
(LTL) ExtractMaximalStateFormulasVisitor
For PRCTL*-model checking, we need to extract the maximal state subformulas in a path formula and substitute those with new labels, e.g., for (F P>0.5[...]) & G (s=0 & d=1) we would get (F a_1) & G a_2 as the resulting formula, with a_1 => P>0.5[...] a_2 => s=0 & d=1 This then allows the recursive computation of the satisfaction sets of the maximal state subformulas and using those in the computation for the (simplified) path formula.tempestpy_adaptions
Joachim Klein
2 changed files with 213 additions and 0 deletions
-
170src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp
-
43src/storm/logic/ExtractMaximalStateFormulasVisitor.h
@ -0,0 +1,170 @@ |
|||||
|
#include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
|
||||
|
|
||||
|
#include "storm/logic/Formulas.h"
|
||||
|
|
||||
|
#include "storm/exceptions/InvalidOperationException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace logic { |
||||
|
|
||||
|
ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(std::vector<LabelFormulaPair>& extractedFormulas) : extractedFormulas(extractedFormulas), nestingLevel(0) { |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, std::vector<LabelFormulaPair>& extractedFormulas) { |
||||
|
ExtractMaximalStateFormulasVisitor visitor(extractedFormulas); |
||||
|
boost::any result = f.accept(visitor, boost::any()); |
||||
|
return boost::any_cast<std::shared_ptr<Formula>>(result); |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const { |
||||
|
if (nestingLevel > 0) { |
||||
|
return CloneVisitor::visit(f, data); |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data)); |
||||
|
if (left->hasQualitativeResult()) { |
||||
|
left = extract(left); |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data)); |
||||
|
if (right->hasQualitativeResult()) { |
||||
|
right = extract(right); |
||||
|
} |
||||
|
|
||||
|
return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanPathFormula>(f.getOperator(), left, right)); |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { |
||||
|
if (nestingLevel > 0) { |
||||
|
return CloneVisitor::visit(f, data); |
||||
|
} |
||||
|
|
||||
|
STORM_LOG_THROW(true, storm::exceptions::InvalidOperationException, "Can not extract maximal state formulas for bounded until"); |
||||
|
// never reached
|
||||
|
return boost::any(); |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { |
||||
|
if (nestingLevel > 0) { |
||||
|
return CloneVisitor::visit(f, data); |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
||||
|
if (sub->hasQualitativeResult()) { |
||||
|
sub = extract(sub); |
||||
|
} |
||||
|
|
||||
|
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(sub)); |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(GloballyFormula const& f, boost::any const& data) const { |
||||
|
if (nestingLevel > 0) { |
||||
|
return CloneVisitor::visit(f, data); |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
||||
|
if (sub->hasQualitativeResult()) { |
||||
|
sub = extract(sub); |
||||
|
} |
||||
|
|
||||
|
return std::static_pointer_cast<Formula>(std::make_shared<GloballyFormula>(sub)); |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(NextFormula const& f, boost::any const& data) const { |
||||
|
if (nestingLevel > 0) { |
||||
|
return CloneVisitor::visit(f, data); |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
||||
|
if (sub->hasQualitativeResult()) { |
||||
|
sub = extract(sub); |
||||
|
} |
||||
|
|
||||
|
return std::static_pointer_cast<Formula>(std::make_shared<NextFormula>(sub)); |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const { |
||||
|
if (nestingLevel > 0) { |
||||
|
return CloneVisitor::visit(f, data); |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
||||
|
if (sub->hasQualitativeResult()) { |
||||
|
sub = extract(sub); |
||||
|
} |
||||
|
|
||||
|
return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanPathFormula>(f.getOperator(), sub)); |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(UntilFormula const& f, boost::any const& data) const { |
||||
|
if (nestingLevel > 0) { |
||||
|
return CloneVisitor::visit(f, data); |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data)); |
||||
|
if (left->hasQualitativeResult()) { |
||||
|
left = extract(left); |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data)); |
||||
|
if (right->hasQualitativeResult()) { |
||||
|
right = extract(right); |
||||
|
} |
||||
|
|
||||
|
return std::static_pointer_cast<Formula>(std::make_shared<UntilFormula>(left, right)); |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { |
||||
|
incrementNestingLevel(); |
||||
|
boost::any result = CloneVisitor::visit(f, data); |
||||
|
decrementNestingLevel(); |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { |
||||
|
incrementNestingLevel(); |
||||
|
boost::any result = CloneVisitor::visit(f, data); |
||||
|
decrementNestingLevel(); |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { |
||||
|
incrementNestingLevel(); |
||||
|
boost::any result = CloneVisitor::visit(f, data); |
||||
|
decrementNestingLevel(); |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { |
||||
|
incrementNestingLevel(); |
||||
|
boost::any result = CloneVisitor::visit(f, data); |
||||
|
decrementNestingLevel(); |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
boost::any ExtractMaximalStateFormulasVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { |
||||
|
incrementNestingLevel(); |
||||
|
boost::any result = CloneVisitor::visit(f, data); |
||||
|
decrementNestingLevel(); |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(std::shared_ptr<Formula> f) const { |
||||
|
std::string label = "p" + std::to_string(extractedFormulas.size()); |
||||
|
|
||||
|
const_cast<std::vector<LabelFormulaPair>&>(extractedFormulas).emplace_back(label, f); |
||||
|
|
||||
|
return std::make_shared<storm::logic::AtomicLabelFormula>(label); |
||||
|
} |
||||
|
|
||||
|
void ExtractMaximalStateFormulasVisitor::incrementNestingLevel() const { |
||||
|
const_cast<std::size_t&>(nestingLevel)++; |
||||
|
} |
||||
|
void ExtractMaximalStateFormulasVisitor::decrementNestingLevel() const { |
||||
|
STORM_LOG_ASSERT(nestingLevel > 0, "Illegal nesting level decrement"); |
||||
|
const_cast<std::size_t&>(nestingLevel)--; |
||||
|
} |
||||
|
|
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,43 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include <vector> |
||||
|
|
||||
|
#include "storm/logic/CloneVisitor.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace logic { |
||||
|
|
||||
|
class ExtractMaximalStateFormulasVisitor : public CloneVisitor { |
||||
|
public: |
||||
|
typedef std::pair<std::string, std::shared_ptr<Formula const>> LabelFormulaPair; |
||||
|
|
||||
|
static std::shared_ptr<Formula> extract(PathFormula const& f, std::vector<LabelFormulaPair>& extractedFormulas); |
||||
|
|
||||
|
virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; |
||||
|
|
||||
|
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; |
||||
|
virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; |
||||
|
|
||||
|
private: |
||||
|
ExtractMaximalStateFormulasVisitor(std::vector<LabelFormulaPair>& extractedFormulas); |
||||
|
|
||||
|
std::shared_ptr<Formula> extract(std::shared_ptr<Formula> f) const; |
||||
|
void incrementNestingLevel() const; |
||||
|
void decrementNestingLevel() const; |
||||
|
|
||||
|
std::vector<LabelFormulaPair>& extractedFormulas; |
||||
|
std::size_t nestingLevel; |
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue