我正在对GRAFCET图(用于对可编程逻辑控制器的行为建模(的转换条件进行可满足性检查。为此，我使用Z3 SMT解算器。
除了正常运算符(AND、OR、NOT和EQUALITY(外，GRAFCET规范在其条件下还允许上升和下降运算符。
示例：↑a(上升边缘(
说明：如果变量a将其值从FALSE更改为TRUE，则条件被统计。
我的第一个想法是检查，是否有一个变量组合可以统计a，也有一个可变组合可以统计NOT(a(。通过这种方式，我可以证明上升边缘可能发生。
[Q] ：是否可以在命题逻辑中直接翻译这些运算符，或者类似于在一个论坛中检查可满足性的东西。
上升/下降边缘表示随时间变化。在SAT/SMT上下文中，变量不会更改。要对您想要的进行建模，您必须捕获不同变量中连续点的值，并检查第一个为False，第二个为True，以进行提升等。
也可以使用由整数索引的数组来表示值。这完全取决于如何将这些图表转换为SAT。在任何情况下，模型中每个变量的值都是恒定的。(也就是说，同时检查a和Not(a)总是不令人满意的。(