sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

(LTL) Add Formula::toPrefixString() 

Convert a formula into prefix format (LBTT/ltl2dstar-style LTL syntax).

 Conflicts:
	src/storm/logic/Formula.h
main
Joachim Klein 5 years ago
committed by Stefan Pranger
parent
bd0a882cd5
commit
b04d2723c2
4 changed files with 205 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 7
      src/storm/logic/Formula.cpp
  2. 1
      src/storm/logic/Formula.h
  3. 155
      src/storm/logic/ToPrefixStringVisitor.cpp
  4. 42
      src/storm/logic/ToPrefixStringVisitor.h

7
src/storm/logic/Formula.cpp
View File

@ -8,6 +8,7 @@
#include "storm/logic/LabelSubstitutionVisitor.h"
#include "storm/logic/RewardModelNameSubstitutionVisitor.h"
#include "storm/logic/ToExpressionVisitor.h"
#include "storm/logic/ToPrefixStringVisitor.h"
namespace storm {
namespace logic {
@ -567,5 +568,11 @@ namespace storm {
std::ostream& operator<<(std::ostream& out, Formula const& formula) {
return formula.writeToStream(out);
}
std::string Formula::toPrefixString() const {
ToPrefixStringVisitor visitor;
return visitor.toPrefixString(*this);
}
}
}

1
src/storm/logic/Formula.h
View File

@ -237,6 +237,7 @@ namespace storm {
std::string toString() const;
virtual std::ostream& writeToStream(std::ostream& out) const = 0;
std::string toPrefixString() const;
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const;
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const;

155
src/storm/logic/ToPrefixStringVisitor.cpp
View File

@ -0,0 +1,155 @@
#include "storm/logic/ToPrefixStringVisitor.h"
#include "storm/logic/Formulas.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidOperationException.h"
namespace storm {
namespace logic {
std::string ToPrefixStringVisitor::toPrefixString(Formula const& f) const {
boost::any result = f.accept(*this, boost::any());
return boost::any_cast<std::string>(result);
}
boost::any ToPrefixStringVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const {
return std::string("\"" + f.getLabel() + "\"");
}
boost::any ToPrefixStringVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
std::string left = boost::any_cast<std::string>(f.getLeftSubformula().accept(*this, data));
std::string right = boost::any_cast<std::string>(f.getRightSubformula().accept(*this, data));
switch (f.getOperator()) {
case BinaryBooleanStateFormula::OperatorType::And:
return std::string("& ") + left + " " + right;
break;
case BinaryBooleanStateFormula::OperatorType::Or:
return std::string("| ") + left + " " + right;
break;
}
return boost::any();
}
boost::any ToPrefixStringVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
std::string left = boost::any_cast<std::string>(f.getLeftSubformula().accept(*this, data));
std::string right = boost::any_cast<std::string>(f.getRightSubformula().accept(*this, data));
switch (f.getOperator()) {
case BinaryBooleanPathFormula::OperatorType::And:
return std::string("& ") + left + " " + right;
break;
case BinaryBooleanPathFormula::OperatorType::Or:
return std::string("| ") + left + " " + right;
break;
}
return boost::any();
}
boost::any ToPrefixStringVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const {
storm::expressions::Expression result;
if (f.isTrueFormula()) {
return std::string("t");
} else {
return std::string("f");
}
return result;
}
boost::any ToPrefixStringVisitor::visit(BoundedUntilFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(ConditionalFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
return std::string("F ") + subexpression;
}
boost::any ToPrefixStringVisitor::visit(TimeOperatorFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
return std::string("G ") + subexpression;
}
boost::any ToPrefixStringVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(LongRunAverageOperatorFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(MultiObjectiveFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(QuantileFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(NextFormula const& f, boost::any const& data) const {
std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
return std::string("X ") + subexpression;
}
boost::any ToPrefixStringVisitor::visit(ProbabilityOperatorFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(RewardOperatorFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
boost::any ToPrefixStringVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
switch (f.getOperator()) {
case UnaryBooleanStateFormula::OperatorType::Not:
return std::string("! ") + subexpression;
break;
}
return boost::any();
}
boost::any ToPrefixStringVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
switch (f.getOperator()) {
case UnaryBooleanPathFormula::OperatorType::Not:
return std::string("! ") + subexpression;
break;
}
return boost::any();
}
boost::any ToPrefixStringVisitor::visit(UntilFormula const& f, boost::any const& data) const {
std::string left = boost::any_cast<std::string>(f.getLeftSubformula().accept(*this, data));
std::string right = boost::any_cast<std::string>(f.getRightSubformula().accept(*this, data));
return std::string("U ") + left + " " + right;
}
boost::any ToPrefixStringVisitor::visit(HOAPathFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
}
}
}

42
src/storm/logic/ToPrefixStringVisitor.h
View File

@ -0,0 +1,42 @@
#pragma once
#include "storm/logic/FormulaVisitor.h"
#include <string>
namespace storm {
namespace logic {
class ToPrefixStringVisitor : public FormulaVisitor {
public:
std::string toPrefixString(Formula const& f) const;
virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override;
virtual boost::any visit(BooleanLiteralFormula 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(ConditionalFormula const& f, boost::any const& data) const override;
virtual boost::any visit(CumulativeRewardFormula 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(TimeOperatorFormula 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(InstantaneousRewardFormula 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(LongRunAverageRewardFormula 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(QuantileFormula 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(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(UnaryBooleanStateFormula 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(HOAPathFormula const& f, boost::any const& data) const override;
};
}
}
Write Preview
Loading…
Cancel
Save