Theory MLTL_Language_Partition_Algorithm

theory MLTL_Language_Partition_Algorithm

imports Mission_Time_LTL.MLTL_Properties

begin

section ‹Extended MLTL Data Structure with Interval Compositions›

text ‹ Extended datatype that has an additional nat list associated 
with the temporal operators F, U, R to represent integer compositions 
of the interval›
datatype (atoms_mltl: 'a) mltl_ext =
  True_mltl_ext ("Truec") 
| False_mltl_ext ("Falsec") 
| Prop_mltl_ext 'a ("Propc '(_')")                           
| Not_mltl_ext "'a mltl_ext" ("Notc _" [85] 85)                    
| And_mltl_ext "'a mltl_ext" "'a mltl_ext" ("_ Andc _" [82, 82] 81)           
| Or_mltl_ext "'a mltl_ext" "'a mltl_ext" ("_ Orc _" [81, 81] 80)         
| Future_mltl_ext "nat" "nat" "nat list" "'a mltl_ext" ("Fc '[_',_'] '<_'>  _" [88, 88, 88, 88] 87)      
| Global_mltl_ext "nat" "nat" "nat list" "'a mltl_ext" ("Gc '[_',_'] '<_'>  _" [88, 88, 88, 88] 87)      
| Until_mltl_ext "'a mltl_ext" "nat" "nat" "nat list" "'a mltl_ext" ("_ Uc '[_',_'] '<_'> _" [84, 84, 84, 84] 83)           
| Release_mltl_ext "'a mltl_ext" "nat" "nat" "nat list" "'a mltl_ext" ("_ Rc '[_',_'] '<_'> _" [84, 84, 84, 84] 83)   

text ‹Converts mltl ext formula to mltl by just dropping the nat list›
fun to_mltl:: "'a mltl_ext ⇒ 'a mltl" where
  "to_mltl Truec = Truem"
| "to_mltl Falsec = Falsem"
| "to_mltl Propc (p) = Propm (p)"
| "to_mltl (Notc φ) = Notm (to_mltl φ)"
| "to_mltl (φ Andc ψ) = (to_mltl φ) Andm (to_mltl ψ)"
| "to_mltl (φ Orc ψ) = (to_mltl φ) Orm (to_mltl ψ)"
| "to_mltl (Fc [a,b] <L> φ) = (Fm [a,b] (to_mltl φ))"
| "to_mltl (Gc [a,b] <L> φ) = (Gm [a,b] (to_mltl φ))"
| "to_mltl (φ Uc [a,b] <L> ψ) = ((to_mltl φ) Um [a,b] (to_mltl ψ))"
| "to_mltl (φ Rc [a,b] <L> ψ) = ((to_mltl φ) Rm [a,b] (to_mltl ψ))"


definition semantics_mltl_ext:: "'a set list ⇒ 'a mltl_ext ⇒ bool" 
  ("_ ⊨c _" [80,80] 80)
  where "π ⊨c φ = π ⊨m (to_mltl φ)"

definition semantic_equiv_ext:: "'a mltl_ext ⇒ 'a mltl_ext ⇒ bool" 
  ("_ ≡c _" [80, 80] 80)
  where "φ ≡c ψ = (to_mltl φ) ≡m(to_mltl ψ)"

definition language_mltl_r :: "'a mltl ⇒ nat ⇒ 'a set list set"
  where "language_mltl_r φ r = 
  {π. semantics_mltl π φ ∧ length π ≥ r}"

fun convert_nnf_ext:: "'a mltl_ext ⇒ 'a mltl_ext" where
  "convert_nnf_ext Truec = Truec"
  | "convert_nnf_ext Falsec = Falsec"
  | "convert_nnf_ext Propc (p) = Propc (p)"
  | "convert_nnf_ext (φ Andc ψ) = ((convert_nnf_ext φ) Andc (convert_nnf_ext ψ))"
  | "convert_nnf_ext (φ Orc ψ) = ((convert_nnf_ext φ) Orc (convert_nnf_ext ψ))"
  | "convert_nnf_ext (Fc [a,b] <L> φ) = (Fc [a,b] <L> (convert_nnf_ext φ))"
  | "convert_nnf_ext (Gc [a,b] <L> φ) = (Gc [a,b] <L> (convert_nnf_ext φ))"
  | "convert_nnf_ext (φ Uc [a,b] <L> ψ) = ((convert_nnf_ext φ) Uc [a,b] <L> (convert_nnf_ext ψ))"
  | "convert_nnf_ext (φ Rc [a,b] <L> ψ) = ((convert_nnf_ext φ) Rc [a,b] <L> (convert_nnf_ext ψ))"
  (* Rewriting with logical duals *)
  | "convert_nnf_ext (Notc Truec) = Falsec" 
  | "convert_nnf_ext (Notc Falsec) = Truec" 
  | "convert_nnf_ext (Notc Propc (p)) = (Notc Propc (p))"
  | "convert_nnf_ext (Notc (Notc φ)) = convert_nnf_ext φ"
  | "convert_nnf_ext (Notc (φ Andc ψ)) = ((convert_nnf_ext (Notc φ)) Orc (convert_nnf_ext (Notc ψ)))"
  | "convert_nnf_ext (Notc (φ Orc ψ)) = ((convert_nnf_ext (Notc φ)) Andc (convert_nnf_ext (Notc ψ)))"
  | "convert_nnf_ext (Notc (Fc [a,b] <L> φ)) = (Gc [a,b] <L> (convert_nnf_ext (Notc φ)))"
  | "convert_nnf_ext (Notc (Gc [a,b] <L> φ)) = (Fc [a,b] <L> (convert_nnf_ext (Notc φ)))"
  | "convert_nnf_ext (Notc (φ Uc [a,b] <L> ψ)) = ((convert_nnf_ext (Notc φ)) Rc [a,b] <L> (convert_nnf_ext (Notc ψ)))"
  | "convert_nnf_ext (Notc (φ Rc [a,b] <L> ψ)) = ((convert_nnf_ext (Notc φ)) Uc [a,b] <L> (convert_nnf_ext (Notc ψ)))"


section ‹List Helper Functions and Properties›
text ‹Computes the partial sum of the first i elements of list›
definition partial_sum :: "[nat list, nat] ⇒ nat" where
  "partial_sum L i = sum_list (take i L)"

text ‹Given interval start time a, and a list of ints L = [t1, t2, t3]
Constructs the list (of length 1 longer) of partial sums added to a:
  [a, a+t1, a+t1+t2, a+t1+t2+t3]›
definition interval_times :: "[nat, nat list] ⇒ nat list" where
  "interval_times a L = map (λi. a + partial_sum L i) [0 ..< length L + 1]"

value "interval_times 3 [1, 2, 3, 4, 5] = 
       [3, 4, 6, 9, 13, 18]"

text ‹This function checks that L is a composition of n.
A composition of an integer n is a way of writing n 
as the sum of a sequence of (strictly) positive integers›
definition is_composition :: "[nat, nat list] ⇒ bool" where
  "is_composition n L = ((∀i. List.member L i ⟶ i > 0) ∧ (sum_list L = n))"

text ‹Checks that every nat list in input of type mltl ext is a composition of its interval
For example the formula F[2,7] has interval of length 7-2+1=6, and a valid
composition would be L = [2, 3, 1]›
fun is_composition_MLTL:: "'a mltl_ext ⇒ bool" where
  "is_composition_MLTL (φ Andc ψ) = ((is_composition_MLTL φ) ∧ (is_composition_MLTL ψ))"
| "is_composition_MLTL (φ Orc ψ) = ((is_composition_MLTL φ) ∧ (is_composition_MLTL ψ))"
| "is_composition_MLTL (Gc[a,b] <L> φ) = ((is_composition (b-a+1) L) ∧ (is_composition_MLTL φ))"
| "is_composition_MLTL (Notc φ) = is_composition_MLTL φ"
| "is_composition_MLTL (Fc[a,b] <L> φ) = ((is_composition (b-a+1) L) ∧ (is_composition_MLTL φ))"
| "is_composition_MLTL (φ Uc[a,b] <L> ψ) = ((is_composition (b-a+1) L) ∧ (is_composition_MLTL φ) ∧ (is_composition_MLTL ψ))"
| "is_composition_MLTL (φ Rc[a,b] <L> ψ) = ((is_composition (b-a+1) L) ∧ (is_composition_MLTL φ) ∧ (is_composition_MLTL ψ))"
| "is_composition_MLTL _ = True" (*Catches prop, true, false cases*)

definition is_composition_allones:: "nat ⇒ nat list ⇒ bool" where
  "is_composition_allones n L = ((is_composition n L) ∧ (∀i<length L. L!i = 1))"

fun is_composition_MLTL_allones:: "'a mltl_ext ⇒ bool" where
  "is_composition_MLTL_allones (φ Andc ψ) = ((is_composition_MLTL_allones φ) ∧ (is_composition_MLTL_allones ψ))"
| "is_composition_MLTL_allones (φ Orc ψ) = ((is_composition_MLTL_allones φ) ∧ (is_composition_MLTL_allones ψ))"
| "is_composition_MLTL_allones (Gc[a,b] <L> φ) = ((is_composition_allones (b-a+1) L) ∧ is_composition_MLTL_allones φ)"
| "is_composition_MLTL_allones (Notc φ) = is_composition_MLTL_allones φ"
| "is_composition_MLTL_allones (Fc[a,b] <L> φ) = ((is_composition_allones (b-a+1) L) ∧ (is_composition_MLTL_allones φ))"
| "is_composition_MLTL_allones (φ Uc[a,b] <L> ψ) = ((is_composition_allones (b-a+1) L) ∧ (is_composition_MLTL_allones φ) ∧ (is_composition_MLTL_allones ψ))"
| "is_composition_MLTL_allones (φ Rc[a,b] <L> ψ) = ((is_composition_allones (b-a+1) L) ∧ (is_composition_MLTL_allones φ) ∧ (is_composition_MLTL_allones ψ))"
| "is_composition_MLTL_allones _ = True" (*Catches prop, true, false cases*)


section ‹Decomposition Function›

fun pairs :: "'a list ⇒ 'a list ⇒ ('a × 'a) list" where
  "pairs [] L2 = []"
| "pairs (h1#T1) L2 = (map (λx. (h1, x)) L2) @ (pairs T1 L2)"

fun And_mltl_list :: "'a mltl_ext list ⇒ 'a mltl_ext list ⇒ 'a mltl_ext list" where
"And_mltl_list D_φ D_ψ = map (λx. And_mltl_ext (fst x) (snd x)) (pairs D_φ D_ψ)"

fun Global_mltl_list :: "'a mltl_ext list ⇒ nat ⇒ nat ⇒ nat list ⇒ 'a mltl_ext list" where
"Global_mltl_list D_φ a b L = map (λx. Global_mltl_ext a b L x) D_φ"

fun Future_mltl_list :: "'a mltl_ext list ⇒ nat ⇒ nat ⇒ nat list ⇒ 'a mltl_ext list" where
"Future_mltl_list D_φ a b L = map (λx. Future_mltl_ext a b L x) D_φ"

fun Until_mltl_list :: "'a mltl_ext ⇒ 'a mltl_ext list ⇒ nat ⇒ nat ⇒ nat list ⇒ 'a mltl_ext list" where
"Until_mltl_list φ D_ψ a b L = map (λx. Until_mltl_ext φ a b L x) D_ψ"

fun Release_mltl_list :: "'a mltl_ext list ⇒ 'a mltl_ext ⇒ nat ⇒ nat ⇒ nat list ⇒ 'a mltl_ext list" where
"Release_mltl_list D_φ ψ a b L = map (λx. Release_mltl_ext x a b L ψ) D_φ"

fun Mighty_Release_mltl_ext:: "'a mltl_ext ⇒ 'a mltl_ext ⇒ nat ⇒ nat ⇒ nat list ⇒ 'a mltl_ext"
  where "Mighty_Release_mltl_ext x ψ a b L =
             (And_mltl_ext (Release_mltl_ext x a b L ψ) 
                           (Future_mltl_ext a b L x))"

fun Mighty_Release_mltl_list :: "'a mltl_ext list ⇒ 'a mltl_ext ⇒ nat ⇒ nat ⇒ nat list ⇒ 'a mltl_ext list" where
"Mighty_Release_mltl_list D_φ ψ a b L = map (λx. Mighty_Release_mltl_ext x ψ a b L) D_φ"

fun Global_mltl_decomp :: "'a mltl_ext list ⇒ nat ⇒ nat ⇒ nat list ⇒ 'a mltl_ext list" where 
  "Global_mltl_decomp D_φ a 0 L = Global_mltl_list D_φ a a [1]"
| "Global_mltl_decomp D_φ a len L = And_mltl_list (Global_mltl_decomp D_φ a (len-1) L) 
   (Global_mltl_list D_φ (a+len) (a+len) [1])"
value "Global_mltl_decomp [True_mltl_ext, (Prop_mltl_ext (0::nat))] 0 2 [3] = 
[(Gc [0,0] <[1]>  Truec Andc Gc [1,1] <[1]>  Truec) Andc Gc [2,2] <[1]>  Truec,
  (Gc [0,0] <[1]>  Truec Andc Gc [1,1] <[1]>  Truec) Andc Gc [2,2] <[1]>  Propc (0),
  (Gc [0,0] <[1]>  Truec Andc Gc [1,1] <[1]>  Propc (0)) Andc Gc [2,2] <[1]>  Truec,
  (Gc [0,0] <[1]>  Truec Andc Gc [1,1] <[1]>  Propc (0)) Andc Gc [2,2] <[1]>  Propc (0),
  (Gc [0,0] <[1]>  Propc (0) Andc Gc [1,1] <[1]>  Truec) Andc Gc [2,2] <[1]>  Truec,
  (Gc [0,0] <[1]>  Propc (0) Andc Gc [1,1] <[1]>  Truec) Andc Gc [2,2] <[1]>  Propc (0),
  (Gc [0,0] <[1]>  Propc (0) Andc Gc [1,1] <[1]>  Propc (0)) Andc Gc [2,2] <[1]>  Truec,
  (Gc [0,0] <[1]>  Propc (0) Andc Gc [1,1] <[1]>  Propc (0)) Andc Gc [2,2] <[1]>  Propc (0)]"

fun LP_mltl_aux :: "'a mltl_ext ⇒ nat ⇒ 'a mltl_ext list" where 
  "LP_mltl_aux φ 0 = [φ]"
| "LP_mltl_aux Truec (Suc k) = [Truec]"
| "LP_mltl_aux Falsec (Suc k) = [Falsec]"
| "LP_mltl_aux Propc (p) (Suc k) = [Propc (p)]"
| "LP_mltl_aux (Notc (Propc (p))) (Suc k) = [Notc (Propc (p))]"
| "LP_mltl_aux (φ Andc ψ) (Suc k)=
   (let D_φ = (LP_mltl_aux (convert_nnf_ext φ) k) in 
   (let D_ψ = (LP_mltl_aux (convert_nnf_ext ψ) k) in 
   And_mltl_list D_φ D_ψ))"
| "LP_mltl_aux (φ Orc ψ) (Suc k) = 
   (let D_φ = (LP_mltl_aux (convert_nnf_ext φ) k) in 
   (let D_ψ = (LP_mltl_aux (convert_nnf_ext ψ) k) in
   (And_mltl_list D_φ D_ψ) @ (And_mltl_list [Notc φ] D_ψ) @ 
   (And_mltl_list D_φ [(Notc ψ)])))"
| "LP_mltl_aux (Gc[a,b] <L> φ) (Suc k) = 
   (let D_φ = (LP_mltl_aux (convert_nnf_ext φ) k) in 
   (if (length D_φ ≤ 1) then ([Gc[a,b] <L> φ]) 
                         else (Global_mltl_decomp D_φ a (b-a) L)))"
| "LP_mltl_aux (Fc[a,b] <L> φ) (Suc k) = 
   (let D_φ = (LP_mltl_aux (convert_nnf_ext φ) k) in 
   (let s = interval_times a L in
   (Future_mltl_list D_φ (s!0) ((s!1)-1) [(s!1)-(s!0)]) @ (concat (map 
    (λi. (And_mltl_list [Global_mltl_ext (s!0) ((s!i)-1) [s!i - s!0] (Notc φ)]
    (Future_mltl_list D_φ (s!i) ((s!(i+1))-1) [s!(i+1)-(s!i)])))
    [1 ..< length L]))))"
| "LP_mltl_aux (φ Uc[a,b] <L> ψ) (Suc k) = 
   (let D_ψ = (LP_mltl_aux (convert_nnf_ext ψ) k) in 
   (let s = interval_times a L in
   (Until_mltl_list φ D_ψ (s!0) ((s!1)-1) [(s!1)-(s!0)]) @ (concat (map
    (λi. (And_mltl_list [Global_mltl_ext (s!0) ((s!i)-1) [s!i - s!0] (And_mltl_ext φ (Notc ψ))]
                   (Until_mltl_list φ D_ψ (s!i) ((s!(i+1)-1)) [s!(i+1)-(s!i)])))
    [1 ..< length L]))))"
| "LP_mltl_aux (φ Rc[a,b] <L> ψ) (Suc k) = 
   (let D_φ = (LP_mltl_aux (convert_nnf_ext φ) k) in 
   (let s = interval_times a L in 
    [Global_mltl_ext a b L ((Notc φ) Andc ψ)] @ 
   (Mighty_Release_mltl_list D_φ ψ (s!0) ((s!1)-1) [(s!1)-(s!0)]) @ (concat (map
    (λi. (And_mltl_list [Global_mltl_ext (s!0) ((s!i)-1) [s!i - s!0] ((Notc φ) Andc ψ)] 
                   (Mighty_Release_mltl_list D_φ ψ (s!i) ((s!(i+1)-1)) [s!(i+1)-(s!i)])))
    [1 ..< length L]))))"
| "LP_mltl_aux _ _ = []"

fun LP_mltl :: "'a mltl_ext ⇒ nat ⇒ 'a mltl list" where
"LP_mltl φ k = map (λx. to_mltl x) 
(map (λx. convert_nnf_ext x) (LP_mltl_aux (convert_nnf_ext φ) k))"


subsection ‹Examples›

value "LP_mltl_aux (Fc[0,9] <[3, 3, 3]> ((Propc (0::nat)) Orc (Propc (1::nat)))) 1 =
[Fc [0,2] <[3]>  (Propc (0) Orc Propc (1)),
 Gc [0,2] <[3]>  (Notc (Propc (0) Orc Propc (1))) Andc Fc [3,5] <[3]>  (Propc (0) Orc Propc (1)),
 Gc [0,5] <[6]>  (Notc (Propc (0) Orc Propc (1))) Andc Fc [6,8] <[3]>  (Propc (0) Orc Propc (1))]"

value "LP_mltl (Truec Orc (Propc (0::nat))) 1 =
[Truem Andm Propm (0), Falsem Andm Propm (0), Truem Andm Notm Propm (0)]"

value "LP_mltl ((Propc (0::nat)) Uc [2,5] <[4]> (Propc (1))) 1 =
       [Propm (0) Um [2,5] Propm (1)]"

value "LP_mltl ((Propc (0::nat)) Rc[2,5] <[2, 2]> (Propc (1))) 1 =
[Gm [2,5] (Notm Propm (0) Andm Propm (1)),
  Propm (0) Rm [2,3] Propm (1) Andm Fm [2,3] Propm (0),
  Gm [2,3] (Notm Propm (0) Andm Propm (1)) Andm (Propm (0) Rm [4,5] Propm (1) Andm Fm [4,5] Propm (0))]"

value "LP_mltl ((Fc[0,3] <[1,1,1,1]> (Propc (0::nat))) Orc
                (Gc[0,3] <[1,1,1,1]> (Propc (1)))) 3 = 
[Fm [0,0] Propm (0) Andm Gm [0,3] Propm (1),
  (Gm [0,0] (Notm Propm (0)) Andm Fm [1,1] Propm (0)) Andm Gm [0,3] Propm (1),
  (Gm [0,1] (Notm Propm (0)) Andm Fm [2,2] Propm (0)) Andm Gm [0,3] Propm (1),
  (Gm [0,2] (Notm Propm (0)) Andm Fm [3,3] Propm (0)) Andm Gm [0,3] Propm (1),
  Gm [0,3] (Notm Propm (0)) Andm Gm [0,3] Propm (1),
  Fm [0,0] Propm (0) Andm Fm [0,3] (Notm Propm (1)),
  (Gm [0,0] (Notm Propm (0)) Andm Fm [1,1] Propm (0)) Andm Fm [0,3] (Notm Propm (1)),
  (Gm [0,1] (Notm Propm (0)) Andm Fm [2,2] Propm (0)) Andm Fm [0,3] (Notm Propm (1)),
  (Gm [0,2] (Notm Propm (0)) Andm Fm [3,3] Propm (0)) Andm Fm [0,3] (Notm Propm (1))]"

end