Dynamic Message Matching Doesn't Help Much

Global: Input information I= known, S= all services
• Set Ψ := Goal in Disjunctive Normal Form, π = ∅, ST=0, CH=0 ,
  where ST will mark successive states from a given parallel state CH.

Procedure Find (Ψ, π, ST)
• If Ψ = ∅ then Success, return π, Else
• If proposition(Ψ), call FindOne(Ψ, π, ST), Else
• If Ψ ≡ ∨{ψ_i}, DO Find(ψ_i, I, π, ST, CH) until result ≠ ∅ or Fail, return ∅ , Else
• If Ψ ≡ ∧{ψ_i}, then If ∀ i, Result_i=Find(ψ_i, π, ST, CH+1)≠ ∅, return ∪{Result_i} Else, Fail, return ∅.

Procedure FindOne (Ψ, π, ST, CH) if S = ∅ Fail, Return ∅, Else, ∀ Si ∈ S: Find OS={Si |Ψ ∈ Output(Si)} If OS = ∅, Fail, Return ∅, Else let ψi = Input(Si) - I, DO Find(∧ψi, π + (Si, ST, CH), ST+1, CH) Si ∈ OS until result ≠ ∅ or Fail, return ∅ .

Even though compositions are dynamic, the lack of preconditions and effects preclude that verification.

---

---

©2012 Charles Petrie - permission to reproduce widely with attribution.