Browse Source

expression conjucntion and disjunction

refactoring
Sebastian Junges 5 years ago
parent
commit
7ae4d0806e
  1. 4
      examples/analysis/02-analysis.py
  2. 4
      src/storage/expressions.cpp

4
examples/analysis/02-analysis.py

@ -28,8 +28,8 @@ def example_analysis_02():
variables[v.name] = v.expression_variable.get_expression() variables[v.name] = v.expression_variable.get_expression()
expr_manager = prism_program.expression_manager expr_manager = prism_program.expression_manager
expr_for_state_1 = Expression.And(Expression.Eq(variables["s"],expr_manager.create_integer(1)),
Expression.Eq(variables["d"],expr_manager.create_integer(0)))
expr_for_state_1 = Expression.Conjunction([Expression.Eq(variables["s"],expr_manager.create_integer(1)),
Expression.Eq(variables["d"],expr_manager.create_integer(0))])
expr_for_state_2 = Expression.And(Expression.Eq(variables["s"],expr_manager.create_integer(4)), expr_for_state_2 = Expression.And(Expression.Eq(variables["s"],expr_manager.create_integer(4)),
Expression.Eq(variables["d"],expr_manager.create_integer(0))) Expression.Eq(variables["d"],expr_manager.create_integer(0)))

4
src/storage/expressions.cpp

@ -1,3 +1,4 @@
#include <vector>
#include "expressions.h" #include "expressions.h"
#include "src/helpers.h" #include "src/helpers.h"
@ -116,6 +117,9 @@ void define_expressions(py::module& m) {
.def_static("Leq", [](Expression const& lhs, Expression const& rhs) {return lhs <= rhs;}) .def_static("Leq", [](Expression const& lhs, Expression const& rhs) {return lhs <= rhs;})
.def_static("Implies", [](Expression const& lhs, Expression const& rhs) {return storm::expressions::implies(lhs, rhs);}) .def_static("Implies", [](Expression const& lhs, Expression const& rhs) {return storm::expressions::implies(lhs, rhs);})
.def_static("Iff", [](Expression const& lhs, Expression const& rhs) {return storm::expressions::iff(lhs, rhs);}) .def_static("Iff", [](Expression const& lhs, Expression const& rhs) {return storm::expressions::iff(lhs, rhs);})
.def_static("Conjunction", [](std::vector<Expression> const& expr) {return storm::expressions::conjunction(expr); })
.def_static("Disjunction", [](std::vector<Expression> const& expr) {return storm::expressions::conjunction(expr); })
; ;

Loading…
Cancel
Save