SAT.dyalog

⎕io←0                               ⍝ 0-indexed arrays, of course
⍝ ----------- The model ----------
⍝ States are represented as their index.
⍝ Labels, as a vector where index i contains all satisfied atomics for state i.
⍝ Relations, as a vector where index i contains all transitions from state i.
⍝ A set of states is represented a boolean selection vector over S.
⍝ --------------------------------
S←⍳4                                ⍝ We have four states
L←(0 1) (0 2) (⊂1) (⊂2)             ⍝ Labelling, 0 is req, 1 is ready and 2 busy
R←(1 3) ( 1 3) (1 2 3) (0 1 2 3 4)  ⍝ Relations, transition from each index
⍝ ------------- Solver ------------
⍝ Only the required primites EX, AF and EU are implemented.
⍝ Negation, conjuction and disjunction we get for free
⍝ since our sets are represented as boolean vectors.
⍝ ---------------------------------
a←{⍵∊¨L} ⋄ SAT←/∘S                  ⍝ Get all states satisfying an atom, gets satisfied state ids
p←{⍺⍺/¨(⍸⍵){⍵∊⍺⍺}¨R}                ⍝ Pre operator, gets all states that transitions to ⍵
pA←∧p ⋄ pE←∨p ⋄ EX←pE               ⍝ Pre-forall and pre-exists, by ∧ and ∨ reducing resp.
AF←{⍵∨pA⍵}⍣≡ ⋄ EU←{⍵∨⍺∧pE⍵}⍣≡       ⍝ AF, EU operators are simple fixpoint functions
⍝ ------------ Syntax -------------
⍝ We want our expressions to be as readable as
⍝ possible, so lets make a function for each atom.
⍝ ---------------------------------
req←a 0 ⋄ ready←a 1 ⋄ busy←a 2
⍝ -------- Usage example ----------
⍝ First, this requires a little manual rewriting since we don't have →:
⍝ SAT(req → AF busy) = SAT(~req ∨ AF busy)
⍝ ---------------------------------
SAT (~req)∨AF busy                 ⍝ Let's give it a spin:
⍝ Should yield:
⍝    0 1 2 3
⍝ So all states satisfy it.