CODEWITHSUNDEEP
z3boolean-logicsmtsatfirst-order-logic
HawkboyZ
HawkboyZ

Reputation: 17

Is it possible to express rising/falling edge operators as SAT/SMT formula?

I am working on a satisfiability check for transition conditions of GRAFCET Diagrams (which is used to model the behaviour of a programmable logic controller). For this purpose I am using the Z3 SMT Solver.

In addition to normal operators (AND, OR, NOT and EQUALITY) the GRAFCET specification allows RISING and FALLING EDGE operators in its conditions.

Exemple: ↑a (RISING EDGE)

Explanation: The conditions is statisfied if the variable a changes its value from FALSE to TRUE.

My first thought would be to check, if there is a variable combination that statisfies a and also a variable combination that statisfies NOT(a). This way I could proof that the RISING EDGE could possibly occure.

[Q]: Is it possible to translate these operators directly in propositional logic or somthing similar to check satisfiablity in one forumula.

Upvotes: 0

Views: 82

Answers (1)

alias
alias

Reputation: 30525

Raising/falling edges suggests change over time. In a SAT/SMT context, variables do not change. To model what you want, you’ll have to capture the value in successive points in different variables and check that the first is False and second is True for raising, etc.

You can also use an array indexed by an integer to represent the value. It all depends on how you translate these diagrams to SAT. In any case, the value of each variable will be constant in the model. (That is, checking a and Not(a) at the same time will always be unsatisfiable.)

Upvotes: 1

Related Questions