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

removed unused file 'variable substitution visitor'

tempestpy_adaptions
TimQu 6 years ago
parent
b5bb87404c
commit
5dda7a5296
2 changed files with 0 additions and 134 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. 94
      src/storm/logic/VariableSubstitutionVisitor.cpp
  2. 40
      src/storm/logic/VariableSubstitutionVisitor.h

94
src/storm/logic/VariableSubstitutionVisitor.cpp
View File

@ -1,94 +0,0 @@
#include "storm/logic/VariableSubstitutionVisitor.h"
#include "storm/logic/Formulas.h"
namespace storm {
namespace logic {
VariableSubstitutionVisitor::VariableSubstitutionVisitor(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) : substitution(substitution) {
// Intentionally left empty.
}
std::shared_ptr<Formula> VariableSubstitutionVisitor::substitute(Formula const& f) const {
boost::any result = f.accept(*this, boost::any());
return boost::any_cast<std::shared_ptr<Formula>>(result);
}
boost::any VariableSubstitutionVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<TimeOperatorFormula>(subformula, substituteOperatorInformation(f.getOperatorInformation())));
}
boost::any VariableSubstitutionVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageOperatorFormula>(subformula, substituteOperatorInformation(f.getOperatorInformation())));
}
boost::any VariableSubstitutionVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<ProbabilityOperatorFormula>(subformula, substituteOperatorInformation(f.getOperatorInformation())));
}
boost::any VariableSubstitutionVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), substituteOperatorInformation(f.getOperatorInformation())));
}
boost::any VariableSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
std::vector<TimeBoundReference> timeBoundReferences;
for (uint64_t i = 0; i < f.getDimension(); ++i) {
if (f.hasLowerBound(i)) {
lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i).substitute(substitution)));
} else {
lowerBounds.emplace_back();
}
if (f.hasUpperBound(i)) {
upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i).substitute(substitution)));
} else {
upperBounds.emplace_back();
}
timeBoundReferences.push_back(f.getTimeBoundReference(i));
}
if (f.hasMultiDimensionalSubformulas()) {
std::vector<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas;
for (uint64_t i = 0; i < f.getDimension(); ++i) {
leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula(i).accept(*this, data)));
rightSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula(i).accept(*this, data)));
}
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
} else {
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
}
}
boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
std::vector<TimeBound> bounds;
std::vector<TimeBoundReference> timeBoundReferences;
for (uint64_t i = 0; i < f.getDimension(); ++i) {
bounds.emplace_back(TimeBound(f.isBoundStrict(i), f.getBound(i).substitute(substitution)));
timeBoundReferences.push_back(f.getTimeBoundReference(i));
}
return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences));
}
boost::any VariableSubstitutionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<InstantaneousRewardFormula>(f.getBound().substitute(substitution), f.getTimeBoundType()));
}
boost::any VariableSubstitutionVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f.getExpression().substitute(substitution)));
}
OperatorInformation VariableSubstitutionVisitor::substituteOperatorInformation(OperatorInformation const& operatorInformation) const {
boost::optional<Bound> bound;
if(operatorInformation.bound) {
bound = Bound(operatorInformation.bound->comparisonType, operatorInformation.bound->threshold.substitute(substitution));
}
return OperatorInformation(operatorInformation.optimalityType, bound);
}
}
}

40
src/storm/logic/VariableSubstitutionVisitor.h
View File

@ -1,40 +0,0 @@
#ifndef STORM_LOGIC_VARIABLESUBSTITUTIONVISITOR_H_
#define STORM_LOGIC_VARIABLESUBSTITUTIONVISITOR_H_
#include <map>
#include "storm/logic/CloneVisitor.h"
#include "storm/storage/expressions/Expression.h"
namespace storm {
namespace logic {
class VariableSubstitutionVisitor : public CloneVisitor {
public:
VariableSubstitutionVisitor(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
std::shared_ptr<Formula> substitute(Formula const& f) const;
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(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(BoundedUntilFormula 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(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
private:
OperatorInformation substituteOperatorInformation(OperatorInformation const& operatorInformation) const;
std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution;
};
}
}
#endif /* STORM_LOGIC_VARIABLESUBSTITUTIONVISITOR_H_ */
Write Preview
Loading…
Cancel
Save