See: Description
Class | Description |
---|---|
CR3SExtRule |
CR-3 : if A ⊑ ∃ r . B ∈ T , (x,
A) ∈ S
then if f(r) then v := (⊤ , {∃ r- . A}) if v ∉ V then V := V ∪ {v} S := S ∪ {(v, B)} ∪ {(v, ⊤)} R := R ∪ {(r, x, v)} else y := (B, ∅) R := R ∪ {(r, x, y)} |
CR4RExtRule |
CR-4 : if ∃ s . A ⊑ B ∈ T, (r,
x, y) ∈ R, (y, A) ∈ S, r ⊑T s
then S := S ∪ {(x, B)} Previous form: CR3 : if (X, Y) ∈ R(r) and A ∈ S(Y) and ∃ r . A ⊑ B ∈ O and B ∉ S(X) then S(X) := S(X) ∪ {B} |
CR4SExtRule |
CR-4 : if ∃ s . A ⊑ B ∈ T, (r, x,
y) ∈ R, (y, A) ∈ S, r ⊑T s
then S := S ∪ {(x, B)} Previous form: CR3 : if (X, Y) ∈ R(r) and A ∈ S(Y) and ∃ r . A ⊑ B ∈ O and B ∉ S(X) then S(X) := S(X) ∪ {B} |
CR5RExtRule |
CR-5 : if s ∘ s ⊑ s ∈ T ,
(r1, x, y) ∈ R, (r2, y, z) ∈ R,
r1 ⊑T s, r2
⊑T s
then R := R ∪ {(s, x, z)} |
CR6RExtRule |
CR-6 : if ∃ s- . A ⊑ B ∈
T, r ⊑T s, (r, x, y) ∈ R, (x, A)
∈ S , (y, B) ∉ S, y = (B', ψ)
then v := (B', ψ ∪ {∃ r - . A}) if v ∉ V then V := V ∪ {v} , S := S ∪ {(v, k) | (y, k) ∈ S} S := S ∪ {(v, B)} R := R ∪ {(r, x, v)} |
CR6SExtRule |
CR-6 : if ∃ s- . A ⊑ B ∈
T, r ⊑T s, (r, x, y) ∈ R, (x, A)
∈ S , (y, B) ∉ S, y = (B', ψ)
then v := (B', ψ ∪ {∃ r - . A}) if v ∉ V then V := V ∪ {v} , S := S ∪ {(v, k) | (y, k) ∈ S} S := S ∪ {(v, B)} R := R ∪ {(r, x, v)} |
CR7RExtRule |
CR-7 : if ∃ s- . A ⊑ B ∈
T , (r2, x, y) ∈ R, x = (A', φ) , y = (B',
ψ),
r ∘ r ⊑ r ∈ T, r1 ⊑T r, r2 ⊑T r, ∃ r1- . A ∈ φ, r ⊑T s then v := (B', ψ ∪ {∃ r- . A}) if v ∉ V then V := V ∪ {v} , S := S ∪ {(v, k) | (y, k) ∈ S} S := S ∪ {(v, B)} R := R ∪ {(r2, x, v)} |
CR8RExtRule |
CR-8 : if A ⊑ ∃ r2- . B
∈ T , (r1, x, y) ∈ R, (y, A) ∈ S,
r1 ⊑T s, r2
⊑T s, f(s-)
then S := S ∪ {(x, B)} |
CR8SExtRule |
CR-8 : if A ⊑ ∃ r2- . B
∈ T , (r1, x, y) ∈ R, (y, A) ∈ S,
r1 ⊑T s, r2
⊑T s, f(s-)
then S := S ∪ {(x, B)} |
CR9RExtOptRule |
CR-9 (optimized) : if (r1, x, y1) ∈
R, (r2, x, y2) ∈ R, …, (rn,
x, yn) ∈ R,
r1 ⊑T s, r2 ⊑T s, …, rn ⊑T s, yi = (⊤ , ψi) for 1 ≤ i ≤ n, yi ≠ yj for 1 ≤ i < j ≤ n, f(s) then v := (⊤ , ψ1 ∪ … ∪ ψn) if v ∉ V then V := V ∪ {v} S := S ∪ {(v, k) | (y1, k) ∈ S} ∪ … ∪ {(v, k) | (yn, k) ∈ S} R := R ∪ {(r1, x, v)} |
CR9RExtRule |
CR-9 : if (r1, x, y) ∈ R, (r2,
x, z) ∈ R, r1 ⊑T s, r2
⊑T s, y = (⊤ , ψ), z = (⊤ , φ), y
≠ z, f(s)
then v := (⊤ , ψ ∪ φ) if v ∉ V then V := V ∪ {v} S := S ∪ {(v, k) | (y, k) ∈ S} ∪ {(v, k) | (z, k) ∈ S} R := R ∪ {(r1, x, v)} |
Copyright © 2009–2015 Chair of Automata Theory - TU Dresden. All rights reserved.