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

added multiple Visitor methods for gameFormulas

main
Stefan Pranger 4 years ago
parent
3a3cd96614
commit
a93a8ed0b0
4 changed files with 145 additions and 145 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 34
      src/storm/logic/CloneVisitor.cpp
  2. 56
      src/storm/logic/FragmentChecker.cpp
  3. 36
      src/storm/logic/LiftableTransitionRewardsVisitor.cpp
  4. 164
      src/storm/storage/jani/JSONExporter.cpp

34
src/storm/logic/CloneVisitor.cpp
View File

@ -4,30 +4,30 @@
namespace storm { namespace storm {
namespace logic { namespace logic {
std::shared_ptr<Formula> CloneVisitor::clone(Formula const& f) const { std::shared_ptr<Formula> CloneVisitor::clone(Formula const& f) const {
boost::any result = f.accept(*this, boost::any()); boost::any result = f.accept(*this, boost::any());
return boost::any_cast<std::shared_ptr<Formula>>(result); return boost::any_cast<std::shared_ptr<Formula>>(result);
} }
boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const { boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f)); return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f));
} }
boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(f)); return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(f));
} }
boost::any CloneVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { boost::any CloneVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data)); 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)); 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<BinaryBooleanStateFormula>(f.getOperator(), left, right)); return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanStateFormula>(f.getOperator(), left, right));
} }
boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const { boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<BooleanLiteralFormula>(f)); return std::static_pointer_cast<Formula>(std::make_shared<BooleanLiteralFormula>(f));
} }
boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds; std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
std::vector<TimeBoundReference> timeBoundReferences; std::vector<TimeBoundReference> timeBoundReferences;
@ -57,17 +57,17 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences)); return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
} }
} }
boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
std::shared_ptr<Formula> conditionFormula = boost::any_cast<std::shared_ptr<Formula>>(f.getConditionFormula().accept(*this, data)); std::shared_ptr<Formula> conditionFormula = boost::any_cast<std::shared_ptr<Formula>>(f.getConditionFormula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<ConditionalFormula>(subformula, conditionFormula, f.getContext())); return std::static_pointer_cast<Formula>(std::make_shared<ConditionalFormula>(subformula, conditionFormula, f.getContext()));
} }
boost::any CloneVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { boost::any CloneVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(f)); return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(f));
} }
boost::any CloneVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { boost::any CloneVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
if (f.hasRewardAccumulation()) { if (f.hasRewardAccumulation()) {
@ -112,41 +112,41 @@ namespace storm {
} }
return std::static_pointer_cast<Formula>(std::make_shared<MultiObjectiveFormula>(subformulas)); return std::static_pointer_cast<Formula>(std::make_shared<MultiObjectiveFormula>(subformulas));
} }
boost::any CloneVisitor::visit(QuantileFormula const& f, boost::any const& data) const { boost::any CloneVisitor::visit(QuantileFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); 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<QuantileFormula>(f.getBoundVariables(), subformula)); return std::static_pointer_cast<Formula>(std::make_shared<QuantileFormula>(f.getBoundVariables(), subformula));
} }
boost::any CloneVisitor::visit(NextFormula const& f, boost::any const& data) const { boost::any CloneVisitor::visit(NextFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); 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<NextFormula>(subformula)); return std::static_pointer_cast<Formula>(std::make_shared<NextFormula>(subformula));
} }
boost::any CloneVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { boost::any CloneVisitor::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)); 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, f.getOperatorInformation())); return std::static_pointer_cast<Formula>(std::make_shared<ProbabilityOperatorFormula>(subformula, f.getOperatorInformation()));
} }
boost::any CloneVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { boost::any CloneVisitor::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)); 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(), f.getOperatorInformation())); return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
} }
boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const { boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f)); return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f));
} }
boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); 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<UnaryBooleanStateFormula>(f.getOperator(), subformula)); return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanStateFormula>(f.getOperator(), subformula));
} }
boost::any CloneVisitor::visit(UntilFormula const& f, boost::any const& data) const { boost::any CloneVisitor::visit(UntilFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data)); 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)); 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<UntilFormula>(left, right)); return std::static_pointer_cast<Formula>(std::make_shared<UntilFormula>(left, right));
} }
} }
} }

56
src/storm/logic/FragmentChecker.cpp
View File

@ -9,7 +9,7 @@ namespace storm {
InheritedInformation(FragmentSpecification const& fragmentSpecification) : fragmentSpecification(fragmentSpecification) { InheritedInformation(FragmentSpecification const& fragmentSpecification) : fragmentSpecification(fragmentSpecification) {
// Intentionally left empty. // Intentionally left empty.
} }
FragmentSpecification const& getSpecification() const { FragmentSpecification const& getSpecification() const {
return fragmentSpecification; return fragmentSpecification;
} }
@ -17,10 +17,10 @@ namespace storm {
private: private:
FragmentSpecification const& fragmentSpecification; FragmentSpecification const& fragmentSpecification;
}; };
bool FragmentChecker::conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const { bool FragmentChecker::conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const {
bool result = boost::any_cast<bool>(f.accept(*this, InheritedInformation(specification))); bool result = boost::any_cast<bool>(f.accept(*this, InheritedInformation(specification)));
if (specification.isOperatorAtTopLevelRequired()) { if (specification.isOperatorAtTopLevelRequired()) {
result &= f.isOperatorFormula(); result &= f.isOperatorFormula();
} }
@ -30,20 +30,20 @@ namespace storm {
if (specification.isQuantileFormulaAtTopLevelRequired()) { if (specification.isQuantileFormulaAtTopLevelRequired()) {
result &= f.isQuantileFormula(); result &= f.isQuantileFormula();
} }
return result; return result;
} }
boost::any FragmentChecker::visit(AtomicExpressionFormula const&, boost::any const& data) const { boost::any FragmentChecker::visit(AtomicExpressionFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areAtomicExpressionFormulasAllowed(); return inherited.getSpecification().areAtomicExpressionFormulasAllowed();
} }
boost::any FragmentChecker::visit(AtomicLabelFormula const&, boost::any const& data) const { boost::any FragmentChecker::visit(AtomicLabelFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areAtomicLabelFormulasAllowed(); return inherited.getSpecification().areAtomicLabelFormulasAllowed();
} }
boost::any FragmentChecker::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areBinaryBooleanStateFormulasAllowed(); bool result = inherited.getSpecification().areBinaryBooleanStateFormulasAllowed();
@ -51,12 +51,12 @@ namespace storm {
result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data)); result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
return result; return result;
} }
boost::any FragmentChecker::visit(BooleanLiteralFormula const&, boost::any const& data) const { boost::any FragmentChecker::visit(BooleanLiteralFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areBooleanLiteralFormulasAllowed(); return inherited.getSpecification().areBooleanLiteralFormulasAllowed();
} }
boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed(); bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed();
@ -78,7 +78,7 @@ namespace storm {
} }
} }
} }
if (f.hasMultiDimensionalSubformulas()) { if (f.hasMultiDimensionalSubformulas()) {
for (uint64_t i = 0; i < f.getDimension(); ++i) { for (uint64_t i = 0; i < f.getDimension(); ++i) {
if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
@ -98,7 +98,7 @@ namespace storm {
} }
return result; return result;
} }
boost::any FragmentChecker::visit(ConditionalFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(ConditionalFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = true; bool result = true;
@ -118,10 +118,10 @@ namespace storm {
result = result && boost::any_cast<bool>(f.getConditionFormula().accept(*this, data)); result = result && boost::any_cast<bool>(f.getConditionFormula().accept(*this, data));
return result; return result;
} }
boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areCumulativeRewardFormulasAllowed(); bool result = inherited.getSpecification().areCumulativeRewardFormulasAllowed();
result = result && (!f.isMultiDimensional() || inherited.getSpecification().areMultiDimensionalCumulativeRewardFormulasAllowed()); result = result && (!f.isMultiDimensional() || inherited.getSpecification().areMultiDimensionalCumulativeRewardFormulasAllowed());
result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
@ -141,7 +141,7 @@ namespace storm {
} }
return result; return result;
} }
boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = true; bool result = true;
@ -163,7 +163,7 @@ namespace storm {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data)); result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
return result; return result;
} }
boost::any FragmentChecker::visit(TimeOperatorFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(TimeOperatorFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areTimeOperatorsAllowed(); bool result = inherited.getSpecification().areTimeOperatorsAllowed();
@ -178,7 +178,7 @@ namespace storm {
} }
return result; return result;
} }
boost::any FragmentChecker::visit(GloballyFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(GloballyFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areGloballyFormulasAllowed(); bool result = inherited.getSpecification().areGloballyFormulasAllowed();
@ -211,16 +211,16 @@ namespace storm {
} }
return result; return result;
} }
boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
return result && inherited.getSpecification().areLongRunAverageRewardFormulasAllowed(); return result && inherited.getSpecification().areLongRunAverageRewardFormulasAllowed();
} }
boost::any FragmentChecker::visit(MultiObjectiveFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
FragmentSpecification subFormulaFragment(inherited.getSpecification()); FragmentSpecification subFormulaFragment(inherited.getSpecification());
if(!inherited.getSpecification().areNestedMultiObjectiveFormulasAllowed()){ if(!inherited.getSpecification().areNestedMultiObjectiveFormulasAllowed()){
subFormulaFragment.setMultiObjectiveFormulasAllowed(false); subFormulaFragment.setMultiObjectiveFormulasAllowed(false);
@ -228,7 +228,7 @@ namespace storm {
if(!inherited.getSpecification().areNestedOperatorsInsideMultiObjectiveFormulasAllowed()){ if(!inherited.getSpecification().areNestedOperatorsInsideMultiObjectiveFormulasAllowed()){
subFormulaFragment.setNestedOperatorsAllowed(false); subFormulaFragment.setNestedOperatorsAllowed(false);
} }
bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed(); bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed();
for(auto const& subF : f.getSubformulas()){ for(auto const& subF : f.getSubformulas()){
if(inherited.getSpecification().areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired()){ if(inherited.getSpecification().areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired()){
@ -238,7 +238,7 @@ namespace storm {
} }
return result; return result;
} }
boost::any FragmentChecker::visit(QuantileFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(QuantileFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
if (!inherited.getSpecification().areQuantileFormulasAllowed()) { if (!inherited.getSpecification().areQuantileFormulasAllowed()) {
@ -246,7 +246,7 @@ namespace storm {
} }
return f.getSubformula().accept(*this, data); return f.getSubformula().accept(*this, data);
} }
boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areNextFormulasAllowed(); bool result = inherited.getSpecification().areNextFormulasAllowed();
@ -256,7 +256,7 @@ namespace storm {
result && boost::any_cast<bool>(f.getSubformula().accept(*this, data)); result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
return result; return result;
} }
boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areProbabilityOperatorsAllowed(); bool result = inherited.getSpecification().areProbabilityOperatorsAllowed();
@ -270,7 +270,7 @@ namespace storm {
} }
return result; return result;
} }
boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areRewardOperatorsAllowed(); bool result = inherited.getSpecification().areRewardOperatorsAllowed();
@ -278,7 +278,7 @@ namespace storm {
result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed()); result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed());
result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula()); result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula());
result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation); result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation);
if (!inherited.getSpecification().areNestedOperatorsAllowed()) { if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
} else { } else {
@ -286,21 +286,21 @@ namespace storm {
} }
return result; return result;
} }
boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
result = result && inherited.getSpecification().areTotalRewardFormulasAllowed(); result = result && inherited.getSpecification().areTotalRewardFormulasAllowed();
return result; return result;
} }
boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areUnaryBooleanStateFormulasAllowed(); bool result = inherited.getSpecification().areUnaryBooleanStateFormulasAllowed();
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data)); result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
return result; return result;
} }
boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const { boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data); InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areUntilFormulasAllowed(); bool result = inherited.getSpecification().areUntilFormulasAllowed();

36
src/storm/logic/LiftableTransitionRewardsVisitor.cpp
View File

@ -5,38 +5,38 @@
namespace storm { namespace storm {
namespace logic { namespace logic {
LiftableTransitionRewardsVisitor::LiftableTransitionRewardsVisitor(storm::storage::SymbolicModelDescription const& symbolicModelDescription) : symbolicModelDescription(symbolicModelDescription) { LiftableTransitionRewardsVisitor::LiftableTransitionRewardsVisitor(storm::storage::SymbolicModelDescription const& symbolicModelDescription) : symbolicModelDescription(symbolicModelDescription) {
// Intentionally left empty. // Intentionally left empty.
} }
bool LiftableTransitionRewardsVisitor::areTransitionRewardsLiftable(Formula const& f) const { bool LiftableTransitionRewardsVisitor::areTransitionRewardsLiftable(Formula const& f) const {
return boost::any_cast<bool>(f.accept(*this, boost::any())); return boost::any_cast<bool>(f.accept(*this, boost::any()));
} }
boost::any LiftableTransitionRewardsVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const { boost::any LiftableTransitionRewardsVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const {
return true; return true;
} }
boost::any LiftableTransitionRewardsVisitor::visit(AtomicLabelFormula const&, boost::any const&) const { boost::any LiftableTransitionRewardsVisitor::visit(AtomicLabelFormula const&, boost::any const&) const {
return true; return true;
} }
boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const { boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const {
return true; return true;
} }
boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const {
return true; return true;
} }
boost::any LiftableTransitionRewardsVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { boost::any LiftableTransitionRewardsVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
for (unsigned i = 0; i < f.getDimension(); ++i) { for (unsigned i = 0; i < f.getDimension(); ++i) {
if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) {
return false; return false;
} }
} }
bool result = true; bool result = true;
if (f.hasMultiDimensionalSubformulas()) { if (f.hasMultiDimensionalSubformulas()) {
for (unsigned i = 0; i < f.getDimension(); ++i) { for (unsigned i = 0; i < f.getDimension(); ++i) {
@ -49,11 +49,11 @@ namespace storm {
} }
return result; return result;
} }
boost::any LiftableTransitionRewardsVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { boost::any LiftableTransitionRewardsVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {
return !f.isConditionalRewardFormula() && boost::any_cast<bool>(f.getSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getConditionFormula().accept(*this, data)); return !f.isConditionalRewardFormula() && boost::any_cast<bool>(f.getSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getConditionFormula().accept(*this, data));
} }
boost::any LiftableTransitionRewardsVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { boost::any LiftableTransitionRewardsVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
for (unsigned i = 0; i < f.getDimension(); ++i) { for (unsigned i = 0; i < f.getDimension(); ++i) {
if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) {
@ -100,35 +100,35 @@ namespace storm {
} }
return result; return result;
} }
boost::any LiftableTransitionRewardsVisitor::visit(QuantileFormula const& f, boost::any const& data) const { boost::any LiftableTransitionRewardsVisitor::visit(QuantileFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data); return f.getSubformula().accept(*this, data);
} }
boost::any LiftableTransitionRewardsVisitor::visit(NextFormula const& f, boost::any const& data) const { boost::any LiftableTransitionRewardsVisitor::visit(NextFormula const& f, boost::any const& data) const {
return boost::any_cast<bool>(f.getSubformula().accept(*this, data)); return boost::any_cast<bool>(f.getSubformula().accept(*this, data));
} }
boost::any LiftableTransitionRewardsVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { boost::any LiftableTransitionRewardsVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data); return f.getSubformula().accept(*this, data);
} }
boost::any LiftableTransitionRewardsVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { boost::any LiftableTransitionRewardsVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
return boost::any_cast<bool>(f.getSubformula().accept(*this, data)); return boost::any_cast<bool>(f.getSubformula().accept(*this, data));
} }
boost::any LiftableTransitionRewardsVisitor::visit(TotalRewardFormula const&, boost::any const&) const { boost::any LiftableTransitionRewardsVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
return true; return true;
} }
boost::any LiftableTransitionRewardsVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { boost::any LiftableTransitionRewardsVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this, data); return f.getSubformula().accept(*this, data);
} }
boost::any LiftableTransitionRewardsVisitor::visit(UntilFormula const& f, boost::any const& data) const { boost::any LiftableTransitionRewardsVisitor::visit(UntilFormula const& f, boost::any const& data) const {
return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this)); return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this));
} }
bool LiftableTransitionRewardsVisitor::rewardModelHasTransitionRewards(std::string const& rewardModelName) const { bool LiftableTransitionRewardsVisitor::rewardModelHasTransitionRewards(std::string const& rewardModelName) const {
if (symbolicModelDescription.hasModel()) { if (symbolicModelDescription.hasModel()) {
if (symbolicModelDescription.isJaniModel()) { if (symbolicModelDescription.isJaniModel()) {

164
src/storm/storage/jani/JSONExporter.cpp
View File

@ -44,7 +44,7 @@ namespace storm {
ExportJsonType res = std::move(*boost::any_cast<ExportJsonType>(&tmp)); ExportJsonType res = std::move(*boost::any_cast<ExportJsonType>(&tmp));
return res; return res;
} }
ExportJsonType buildExpression(storm::expressions::Expression const& exp, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet(), std::unordered_set<std::string> const& auxiliaryVariables = {}) { ExportJsonType buildExpression(storm::expressions::Expression const& exp, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet(), std::unordered_set<std::string> const& auxiliaryVariables = {}) {
STORM_LOG_TRACE("Exporting " << exp); STORM_LOG_TRACE("Exporting " << exp);
return ExpressionToJson::translate(exp, constants, globalVariables, localVariables, auxiliaryVariables); return ExpressionToJson::translate(exp, constants, globalVariables, localVariables, auxiliaryVariables);
@ -53,14 +53,14 @@ namespace storm {
class CompositionJsonExporter : public CompositionVisitor { class CompositionJsonExporter : public CompositionVisitor {
public: public:
CompositionJsonExporter(bool allowRecursion) : allowRecursion(allowRecursion){ CompositionJsonExporter(bool allowRecursion) : allowRecursion(allowRecursion){
} }
static ExportJsonType translate(storm::jani::Composition const& comp, bool allowRecursion = true) { static ExportJsonType translate(storm::jani::Composition const& comp, bool allowRecursion = true) {
CompositionJsonExporter visitor(allowRecursion); CompositionJsonExporter visitor(allowRecursion);
return anyToJson(comp.accept(visitor, boost::none)); return anyToJson(comp.accept(visitor, boost::none));
} }
virtual boost::any visit(AutomatonComposition const& composition, boost::any const&) { virtual boost::any visit(AutomatonComposition const& composition, boost::any const&) {
ExportJsonType compDecl; ExportJsonType compDecl;
ExportJsonType autDecl; ExportJsonType autDecl;
@ -70,10 +70,10 @@ namespace storm {
compDecl["elements"] = elements; compDecl["elements"] = elements;
return compDecl; return compDecl;
} }
virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) { virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) {
ExportJsonType compDecl; ExportJsonType compDecl;
std::vector<ExportJsonType> elems; std::vector<ExportJsonType> elems;
for (auto const& subcomp : composition.getSubcompositions()) { for (auto const& subcomp : composition.getSubcompositions()) {
ExportJsonType elemDecl; ExportJsonType elemDecl;
@ -103,14 +103,14 @@ namespace storm {
if (!synElems.empty()) { if (!synElems.empty()) {
compDecl["syncs"] = synElems; compDecl["syncs"] = synElems;
} }
return compDecl; return compDecl;
} }
private: private:
bool allowRecursion; bool allowRecursion;
}; };
std::string comparisonTypeToJani(storm::logic::ComparisonType ct) { std::string comparisonTypeToJani(storm::logic::ComparisonType ct) {
switch(ct) { switch(ct) {
case storm::logic::ComparisonType::Less: case storm::logic::ComparisonType::Less:
@ -124,12 +124,12 @@ namespace storm {
} }
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType");
} }
ExportJsonType FormulaToJaniJson::constructPropertyInterval(boost::optional<storm::expressions::Expression> const& lower, boost::optional<bool> const& lowerExclusive, boost::optional<storm::expressions::Expression> const& upper, boost::optional<bool> const& upperExclusive) const { ExportJsonType FormulaToJaniJson::constructPropertyInterval(boost::optional<storm::expressions::Expression> const& lower, boost::optional<bool> const& lowerExclusive, boost::optional<storm::expressions::Expression> const& upper, boost::optional<bool> const& upperExclusive) const {
STORM_LOG_THROW((lower.is_initialized() || upper.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval needs either a lower or an upper bound, but none was given."); STORM_LOG_THROW((lower.is_initialized() || upper.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval needs either a lower or an upper bound, but none was given.");
STORM_LOG_THROW((lower.is_initialized() || !lowerExclusive.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval defines wether the lower bound is exclusive but no lower bound is given."); STORM_LOG_THROW((lower.is_initialized() || !lowerExclusive.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval defines wether the lower bound is exclusive but no lower bound is given.");
STORM_LOG_THROW((upper.is_initialized() || !upperExclusive.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval defines wether the upper bound is exclusive but no upper bound is given."); STORM_LOG_THROW((upper.is_initialized() || !upperExclusive.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval defines wether the upper bound is exclusive but no upper bound is given.");
ExportJsonType iDecl; ExportJsonType iDecl;
if (lower) { if (lower) {
iDecl["lower"] = buildExpression(*lower, model.getConstants(), model.getGlobalVariables()); iDecl["lower"] = buildExpression(*lower, model.getConstants(), model.getGlobalVariables());
@ -145,17 +145,17 @@ namespace storm {
} }
return iDecl; return iDecl;
} }
ExportJsonType FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const { ExportJsonType FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const {
storm::jani::RewardModelInformation info(model, rewardModelName); storm::jani::RewardModelInformation info(model, rewardModelName);
bool steps = rewardAccumulation.isStepsSet() && (info.hasActionRewards() || info.hasTransitionRewards()); bool steps = rewardAccumulation.isStepsSet() && (info.hasActionRewards() || info.hasTransitionRewards());
bool time = rewardAccumulation.isTimeSet() && !model.isDiscreteTimeModel() && info.hasStateRewards(); bool time = rewardAccumulation.isTimeSet() && !model.isDiscreteTimeModel() && info.hasStateRewards();
bool exit = rewardAccumulation.isExitSet() && info.hasStateRewards(); bool exit = rewardAccumulation.isExitSet() && info.hasStateRewards();
return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit)); return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit));
} }
ExportJsonType FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const { ExportJsonType FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const {
std::vector<std::string> res; std::vector<std::string> res;
if (rewardAccumulation.isStepsSet()) { if (rewardAccumulation.isStepsSet()) {
@ -178,7 +178,7 @@ namespace storm {
return constructRewardAccumulation(storm::logic::RewardAccumulation(true, true, false), rewardModelName); return constructRewardAccumulation(storm::logic::RewardAccumulation(true, true, false), rewardModelName);
} }
} }
ExportJsonType FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) { ExportJsonType FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {
FormulaToJaniJson translator(model); FormulaToJaniJson translator(model);
auto result = anyToJson(formula.accept(translator)); auto result = anyToJson(formula.accept(translator));
@ -187,15 +187,15 @@ namespace storm {
} }
return result; return result;
} }
bool FormulaToJaniJson::containsStateExitRewards() const { bool FormulaToJaniJson::containsStateExitRewards() const {
return stateExitRewards; return stateExitRewards;
} }
boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const&) const {
return buildExpression(f.getExpression(), model.getConstants(), model.getGlobalVariables()); return buildExpression(f.getExpression(), model.getConstants(), model.getGlobalVariables());
} }
boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const&) const {
ExportJsonType opDecl(f.getLabel()); ExportJsonType opDecl(f.getLabel());
return opDecl; return opDecl;
@ -218,10 +218,10 @@ namespace storm {
opDecl["op"] = "U"; opDecl["op"] = "U";
opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data)); opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data));
opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data)); opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data));
bool hasStepBounds(false), hasTimeBounds(false); bool hasStepBounds(false), hasTimeBounds(false);
std::vector<ExportJsonType> rewardBounds; std::vector<ExportJsonType> rewardBounds;
for (uint64_t i = 0; i < f.getDimension(); ++i) { for (uint64_t i = 0; i < f.getDimension(); ++i) {
boost::optional<storm::expressions::Expression> lower, upper; boost::optional<storm::expressions::Expression> lower, upper;
boost::optional<bool> lowerExclusive, upperExclusive; boost::optional<bool> lowerExclusive, upperExclusive;
@ -234,7 +234,7 @@ namespace storm {
upperExclusive = f.isUpperBoundStrict(i); upperExclusive = f.isUpperBoundStrict(i);
} }
ExportJsonType propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive); ExportJsonType propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive);
auto tbr = f.getTimeBoundReference(i); auto tbr = f.getTimeBoundReference(i);
if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) { if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) {
STORM_LOG_THROW(!hasStepBounds, storm::exceptions::NotSupportedException, "Jani export of until formulas with multiple step bounds is not supported."); STORM_LOG_THROW(!hasStepBounds, storm::exceptions::NotSupportedException, "Jani export of until formulas with multiple step bounds is not supported.");
@ -262,15 +262,15 @@ namespace storm {
return opDecl; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::ConditionalFormula const&, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::ConditionalFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae");
} }
boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const&, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cumulative reward formulae"); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cumulative reward formulae");
} }
boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const {
ExportJsonType opDecl; ExportJsonType opDecl;
opDecl["op"] = "U"; opDecl["op"] = "U";
@ -278,10 +278,10 @@ namespace storm {
opDecl["right"] = anyToJson(f.getSubformula().accept(*this, data)); opDecl["right"] = anyToJson(f.getSubformula().accept(*this, data));
return opDecl; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const {
ExportJsonType opDecl; ExportJsonType opDecl;
// Create standard reward accumulation for time operator formulas. // Create standard reward accumulation for time operator formulas.
storm::logic::RewardAccumulation rewAcc(model.isDiscreteTimeModel(), !model.isDiscreteTimeModel(), false); storm::logic::RewardAccumulation rewAcc(model.isDiscreteTimeModel(), !model.isDiscreteTimeModel(), false);
if (f.getSubformula().isEventuallyFormula() && f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) { if (f.getSubformula().isEventuallyFormula() && f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) {
@ -357,7 +357,7 @@ namespace storm {
if(f.hasOptimalityType()) { if(f.hasOptimalityType()) {
opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data));
} else { } else {
// TODO add checks // TODO add checks
opDecl["op"] = "Smin"; opDecl["op"] = "Smin";
@ -366,7 +366,7 @@ namespace storm {
} }
return opDecl; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const&, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const&, boost::any const&) const {
// ExportJsonType opDecl; // ExportJsonType opDecl;
// if(f.()) { // if(f.()) {
@ -384,7 +384,7 @@ namespace storm {
// if(f.hasOptimalityType()) { // if(f.hasOptimalityType()) {
// opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; // opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
// opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, boost::none)); // opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, boost::none));
//
//
// } else { // } else {
// // TODO add checks // // TODO add checks
// opDecl["op"] = "Pmin"; // opDecl["op"] = "Pmin";
@ -392,19 +392,19 @@ namespace storm {
// } // }
// } // }
// return opDecl; // return opDecl;
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an LRA reward formula"); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an LRA reward formula");
} }
boost::any FormulaToJaniJson::visit(storm::logic::MultiObjectiveFormula const&, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::MultiObjectiveFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a multi-objective formula"); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a multi-objective formula");
} }
boost::any FormulaToJaniJson::visit(storm::logic::QuantileFormula const&, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::QuantileFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a Quantile formula"); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a Quantile formula");
} }
boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const {
ExportJsonType opDecl; ExportJsonType opDecl;
opDecl["op"] = "U"; opDecl["op"] = "U";
@ -414,13 +414,13 @@ namespace storm {
opDecl["step-bounds"] = constructPropertyInterval(intervalExpressionManager->integer(1), false, intervalExpressionManager->integer(1), false); opDecl["step-bounds"] = constructPropertyInterval(intervalExpressionManager->integer(1), false, intervalExpressionManager->integer(1), false);
return opDecl; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const {
ExportJsonType opDecl; ExportJsonType opDecl;
if(f.hasBound()) { if(f.hasBound()) {
auto bound = f.getBound(); auto bound = f.getBound();
opDecl["op"] = comparisonTypeToJani(bound.comparisonType); opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
@ -436,7 +436,7 @@ namespace storm {
if(f.hasOptimalityType()) { if(f.hasOptimalityType()) {
opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax"; opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax";
opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data));
} else { } else {
// TODO add checks // TODO add checks
opDecl["op"] = "Pmin"; opDecl["op"] = "Pmin";
@ -445,10 +445,10 @@ namespace storm {
} }
return opDecl; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const {
ExportJsonType opDecl; ExportJsonType opDecl;
std::string instantName; std::string instantName;
if (model.isDiscreteTimeModel()) { if (model.isDiscreteTimeModel()) {
instantName = "step-instant"; instantName = "step-instant";
@ -514,7 +514,7 @@ namespace storm {
} }
} }
opDecl["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables()); opDecl["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables());
if(f.hasBound()) { if(f.hasBound()) {
ExportJsonType compDecl; ExportJsonType compDecl;
auto bound = f.getBound(); auto bound = f.getBound();
@ -526,11 +526,11 @@ namespace storm {
return opDecl; return opDecl;
} }
} }
boost::any FormulaToJaniJson::visit(storm::logic::TotalRewardFormula const&, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::TotalRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support a total reward formula"); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support a total reward formula");
} }
boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const {
ExportJsonType opDecl; ExportJsonType opDecl;
storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator(); storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator();
@ -539,7 +539,7 @@ namespace storm {
opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data));
return opDecl; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const {
ExportJsonType opDecl; ExportJsonType opDecl;
opDecl["op"] = "U"; opDecl["op"] = "U";
@ -547,9 +547,9 @@ namespace storm {
opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data)); opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data));
return opDecl; return opDecl;
} }
std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) { std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) {
using OpType = storm::expressions::OperatorType; using OpType = storm::expressions::OperatorType;
switch(optype) { switch(optype) {
case OpType::And: case OpType::And:
@ -602,16 +602,16 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Operator not supported by Jani"); STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Operator not supported by Jani");
} }
} }
ExportJsonType ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables) { ExportJsonType ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables) {
// Simplify the expression first and reduce the nesting // Simplify the expression first and reduce the nesting
auto simplifiedExpr = storm::jani::reduceNestingInJaniExpression(expr.simplify()); auto simplifiedExpr = storm::jani::reduceNestingInJaniExpression(expr.simplify());
ExpressionToJson visitor(constants, globalVariables, localVariables, auxiliaryVariables); ExpressionToJson visitor(constants, globalVariables, localVariables, auxiliaryVariables);
return anyToJson(simplifiedExpr.accept(visitor, boost::none)); return anyToJson(simplifiedExpr.accept(visitor, boost::none));
} }
boost::any ExpressionToJson::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) { boost::any ExpressionToJson::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) {
ExportJsonType opDecl; ExportJsonType opDecl;
opDecl["op"] = "ite"; opDecl["op"] = "ite";
@ -679,7 +679,7 @@ namespace storm {
boost::any ExpressionToJson::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) { boost::any ExpressionToJson::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) {
return ExportJsonType(expression.getValue()); return ExportJsonType(expression.getValue());
} }
boost::any ExpressionToJson::visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data) { boost::any ExpressionToJson::visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data) {
ExportJsonType opDecl; ExportJsonType opDecl;
opDecl["op"] = "av"; opDecl["op"] = "av";
@ -691,7 +691,7 @@ namespace storm {
opDecl["elements"] = std::move(elements); opDecl["elements"] = std::move(elements);
return opDecl; return opDecl;
} }
boost::any ExpressionToJson::visit(storm::expressions::ConstructorArrayExpression const& expression, boost::any const& data) { boost::any ExpressionToJson::visit(storm::expressions::ConstructorArrayExpression const& expression, boost::any const& data) {
ExportJsonType opDecl; ExportJsonType opDecl;
opDecl["op"] = "ac"; opDecl["op"] = "ac";
@ -704,7 +704,7 @@ namespace storm {
} }
return opDecl; return opDecl;
} }
boost::any ExpressionToJson::visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) { boost::any ExpressionToJson::visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) {
ExportJsonType opDecl; ExportJsonType opDecl;
opDecl["op"] = "aa"; opDecl["op"] = "aa";
@ -712,7 +712,7 @@ namespace storm {
opDecl["index"] = anyToJson(expression.getOperand(1)->accept(*this, data)); opDecl["index"] = anyToJson(expression.getOperand(1)->accept(*this, data));
return opDecl; return opDecl;
} }
boost::any ExpressionToJson::visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data) { boost::any ExpressionToJson::visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data) {
ExportJsonType opDecl; ExportJsonType opDecl;
opDecl["op"] = "call"; opDecl["op"] = "call";
@ -724,14 +724,14 @@ namespace storm {
opDecl["args"] = std::move(arguments); opDecl["args"] = std::move(arguments);
return opDecl; return opDecl;
} }
void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid, bool compact) { void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid, bool compact) {
std::ofstream stream; std::ofstream stream;
storm::utility::openFile(filepath, stream, false, true); storm::utility::openFile(filepath, stream, false, true);
toStream(janiModel, formulas, stream, checkValid, compact); toStream(janiModel, formulas, stream, checkValid, compact);
storm::utility::closeFile(stream); storm::utility::closeFile(stream);
} }
void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& os, bool checkValid, bool compact) { void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& os, bool checkValid, bool compact) {
if(checkValid) { if(checkValid) {
janiModel.checkValid(); janiModel.checkValid();
@ -752,7 +752,7 @@ namespace storm {
} }
STORM_LOG_INFO("Conversion completed " << janiModel.getName() << "."); STORM_LOG_INFO("Conversion completed " << janiModel.getName() << ".");
} }
ExportJsonType buildActionArray(std::vector<storm::jani::Action> const& actions) { ExportJsonType buildActionArray(std::vector<storm::jani::Action> const& actions) {
std::vector<ExportJsonType> actionReprs; std::vector<ExportJsonType> actionReprs;
uint64_t actIndex = 0; uint64_t actIndex = 0;
@ -766,11 +766,11 @@ namespace storm {
actEntry["name"] = act.getName(); actEntry["name"] = act.getName();
actionReprs.push_back(actEntry); actionReprs.push_back(actEntry);
} }
return ExportJsonType(actionReprs); return ExportJsonType(actionReprs);
} }
ExportJsonType buildTypeDescription(storm::expressions::Type const& type) { ExportJsonType buildTypeDescription(storm::expressions::Type const& type) {
ExportJsonType typeDescr; ExportJsonType typeDescr;
if (type.isIntegerType()) { if (type.isIntegerType()) {
@ -787,7 +787,7 @@ namespace storm {
} }
return typeDescr; return typeDescr;
} }
void getBoundsFromConstraints(ExportJsonType& typeDesc, storm::expressions::Variable const& var, storm::expressions::Expression const& constraint, std::vector<storm::jani::Constant> const& constants) { void getBoundsFromConstraints(ExportJsonType& typeDesc, storm::expressions::Variable const& var, storm::expressions::Expression const& constraint, std::vector<storm::jani::Constant> const& constants) {
if (constraint.getBaseExpression().isBinaryBooleanFunctionExpression() && constraint.getBaseExpression().getOperator() == storm::expressions::OperatorType::And) { if (constraint.getBaseExpression().isBinaryBooleanFunctionExpression() && constraint.getBaseExpression().getOperator() == storm::expressions::OperatorType::And) {
getBoundsFromConstraints(typeDesc, var, constraint.getBaseExpression().getOperand(0), constants); getBoundsFromConstraints(typeDesc, var, constraint.getBaseExpression().getOperand(0), constants);
@ -811,7 +811,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani Export for constant constraint " << constraint << " is not supported."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani Export for constant constraint " << constraint << " is not supported.");
} }
} }
ExportJsonType buildConstantsArray(std::vector<storm::jani::Constant> const& constants) { ExportJsonType buildConstantsArray(std::vector<storm::jani::Constant> const& constants) {
std::vector<ExportJsonType> constantDeclarations; std::vector<ExportJsonType> constantDeclarations;
for(auto const& constant : constants) { for(auto const& constant : constants) {
@ -833,8 +833,8 @@ namespace storm {
} }
return ExportJsonType(constantDeclarations); return ExportJsonType(constantDeclarations);
} }
ExportJsonType buildVariablesArray(storm::jani::VariableSet const& varSet, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) { ExportJsonType buildVariablesArray(storm::jani::VariableSet const& varSet, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
ExportJsonType variableDeclarations = std::vector<ExportJsonType>(); ExportJsonType variableDeclarations = std::vector<ExportJsonType>();
for(auto const& variable : varSet) { for(auto const& variable : varSet) {
@ -916,7 +916,7 @@ namespace storm {
} }
return functionDeclarations; return functionDeclarations;
} }
ExportJsonType buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
ExportJsonType assignmentDeclarations = std::vector<ExportJsonType>(); ExportJsonType assignmentDeclarations = std::vector<ExportJsonType>();
bool addIndex = orderedAssignments.hasMultipleLevels(); bool addIndex = orderedAssignments.hasMultipleLevels();
@ -943,7 +943,7 @@ namespace storm {
} }
return assignmentDeclarations; return assignmentDeclarations;
} }
ExportJsonType buildLocationsArray(std::vector<storm::jani::Location> const& locations, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType buildLocationsArray(std::vector<storm::jani::Location> const& locations, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
ExportJsonType locationDeclarations = std::vector<ExportJsonType>(); ExportJsonType locationDeclarations = std::vector<ExportJsonType>();
for(auto const& location : locations) { for(auto const& location : locations) {
@ -964,7 +964,7 @@ namespace storm {
} }
return locationDeclarations; return locationDeclarations;
} }
ExportJsonType buildInitialLocations(storm::jani::Automaton const& automaton) { ExportJsonType buildInitialLocations(storm::jani::Automaton const& automaton) {
std::vector<std::string> names; std::vector<std::string> names;
for(auto const& initLocIndex : automaton.getInitialLocationIndices()) { for(auto const& initLocIndex : automaton.getInitialLocationIndices()) {
@ -972,7 +972,7 @@ namespace storm {
} }
return ExportJsonType(names); return ExportJsonType(names);
} }
ExportJsonType buildDestinations(std::vector<EdgeDestination> const& destinations, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType buildDestinations(std::vector<EdgeDestination> const& destinations, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
assert(destinations.size() > 0); assert(destinations.size() > 0);
ExportJsonType destDeclarations = std::vector<ExportJsonType>(); ExportJsonType destDeclarations = std::vector<ExportJsonType>();
@ -998,7 +998,7 @@ namespace storm {
} }
return destDeclarations; return destDeclarations;
} }
ExportJsonType buildEdge(Edge const& edge , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType buildEdge(Edge const& edge , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
STORM_LOG_THROW(edge.getDestinations().size() > 0, storm::exceptions::InvalidJaniException, "An edge without destinations is not allowed."); STORM_LOG_THROW(edge.getDestinations().size() > 0, storm::exceptions::InvalidJaniException, "An edge without destinations is not allowed.");
ExportJsonType edgeEntry; ExportJsonType edgeEntry;
@ -1024,7 +1024,7 @@ namespace storm {
} }
return edgeEntry; return edgeEntry;
} }
ExportJsonType buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
ExportJsonType edgeDeclarations = std::vector<ExportJsonType>(); ExportJsonType edgeDeclarations = std::vector<ExportJsonType>();
for(auto const& edge : edges) { for(auto const& edge : edges) {
@ -1035,7 +1035,7 @@ namespace storm {
} }
return edgeDeclarations; return edgeDeclarations;
} }
ExportJsonType buildAutomataArray(std::vector<storm::jani::Automaton> const& automata, std::map<uint64_t, std::string> const& actionNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, bool commentExpressions) { ExportJsonType buildAutomataArray(std::vector<storm::jani::Automaton> const& automata, std::map<uint64_t, std::string> const& actionNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, bool commentExpressions) {
ExportJsonType automataDeclarations = std::vector<ExportJsonType>(); ExportJsonType automataDeclarations = std::vector<ExportJsonType>();
for(auto const& automaton : automata) { for(auto const& automaton : automata) {
@ -1055,7 +1055,7 @@ namespace storm {
} }
return automataDeclarations; return automataDeclarations;
} }
void JsonExporter::convertModel(storm::jani::Model const& janiModel, bool commentExpressions) { void JsonExporter::convertModel(storm::jani::Model const& janiModel, bool commentExpressions) {
modelFeatures = janiModel.getModelFeatures(); modelFeatures = janiModel.getModelFeatures();
jsonStruct["jani-version"] = janiModel.getJaniVersion(); jsonStruct["jani-version"] = janiModel.getJaniVersion();
@ -1071,12 +1071,12 @@ namespace storm {
jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), commentExpressions); jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), commentExpressions);
jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition()); jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition());
} }
ExportJsonType JsonExporter::getEdgeAsJson(storm::jani::Model const& janiModel, uint64_t automatonIndex, uint64_t edgeIndex, bool commentExpressions) { ExportJsonType JsonExporter::getEdgeAsJson(storm::jani::Model const& janiModel, uint64_t automatonIndex, uint64_t edgeIndex, bool commentExpressions) {
auto const& automaton = janiModel.getAutomaton(automatonIndex); auto const& automaton = janiModel.getAutomaton(automatonIndex);
return buildEdge(automaton.getEdge(edgeIndex), janiModel.getActionIndexToNameMap(), automaton.buildIdToLocationNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), automaton.getVariables(), commentExpressions); return buildEdge(automaton.getEdge(edgeIndex), janiModel.getActionIndexToNameMap(), automaton.buildIdToLocationNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), automaton.getVariables(), commentExpressions);
} }
std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) {
switch(ft) { switch(ft) {
case storm::modelchecker::FilterType::MIN: case storm::modelchecker::FilterType::MIN:
@ -1102,7 +1102,7 @@ namespace storm {
} }
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType"); STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType");
} }
ExportJsonType convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) { ExportJsonType convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {
ExportJsonType propDecl; ExportJsonType propDecl;
propDecl["states"]["op"] = "initial"; propDecl["states"]["op"] = "initial";
@ -1111,11 +1111,11 @@ namespace storm {
propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), model, modelFeatures); propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), model, modelFeatures);
return propDecl; return propDecl;
} }
void JsonExporter::convertProperties( std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model) { void JsonExporter::convertProperties( std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model) {
ExportJsonType properties; ExportJsonType properties;
// Unset model-features that only relate to properties. These are only set if such properties actually exist. // Unset model-features that only relate to properties. These are only set if such properties actually exist.
modelFeatures.remove(storm::jani::ModelFeature::StateExitRewards); modelFeatures.remove(storm::jani::ModelFeature::StateExitRewards);
if (formulas.empty()) { if (formulas.empty()) {
@ -1133,7 +1133,7 @@ namespace storm {
} }
jsonStruct["properties"] = std::move(properties); jsonStruct["properties"] = std::move(properties);
} }
ExportJsonType JsonExporter::finalize() { ExportJsonType JsonExporter::finalize() {
jsonStruct["features"] = ExportJsonType::parse(modelFeatures.toString()); jsonStruct["features"] = ExportJsonType::parse(modelFeatures.toString());
return jsonStruct; return jsonStruct;

Write Preview
Loading…
Cancel
Save