Loading theory "Extended_Finite_State_Machine_Inference.Code_Target_List"
Loading theory "Extended_Finite_State_Machine_Inference.Group_By" (required by "Extended_Finite_State_Machine_Inference.PTA_Generalisation")
Loading theory "Extended_Finite_State_Machine_Inference.Code_Target_Set"
Loading theory "Extended_Finite_State_Machine_Inference.Code_Target_FSet"
### Code generator: dropping subsumed code equation
### enumerate ?n (?x # ?xs) \<equiv> (?n, ?x) # enumerate (Suc ?n) ?xs
### Code generator: dropping subsumed code equation
### enumerate ?n [] \<equiv> []
### Code generator: dropping subsumed code equation
### List.maps ?f [] \<equiv> []
### Code generator: dropping subsumed code equation
### List.maps ?f (?x # ?xs) \<equiv> ?f ?x @ List.maps ?f ?xs
### theory "Extended_Finite_State_Machine_Inference.Code_Target_Set"
### 0.105s elapsed time, 0.484s cpu time, 0.000s GC time
Loading theory "Extended_Finite_State_Machine_Inference.Subsumption"
### Code generator: dropping subsumed code equation
### list_all ?P [] \<equiv> True
### Code generator: dropping subsumed code equation
### list_all ?P (?x # ?xs) \<equiv> ?P ?x \<and> list_all ?P ?xs
### Code generator: dropping subsumed code equation
### list_ex ?P [] \<equiv> False
### Code generator: dropping subsumed code equation
### list_ex ?P (?x # ?xs) \<equiv> ?P ?x \<or> list_ex ?P ?xs
### Code generator: dropping subsumed code equation
### fold ?f (?x # ?xs) ?s \<equiv> fold ?f ?xs (?f ?x ?s)
### Code generator: dropping subsumed code equation
### fold ?f [] ?s \<equiv> ?s
### Code generator: dropping subsumed code equation
### ?A |\<subset>| ?B \<equiv> ?A |\<subseteq>| ?B \<and> \<not> ?B |\<subseteq>| ?A
### Code generator: dropping subsumed code equation
### fset (fset_of_list ?x) \<equiv> set ?x
### Code generator: dropping subsumed code equation
### sorted_list_of_set (set ?xs) \<equiv> sort (remdups ?xs)
### Code generator: dropping subsumed code equation
### fMin (fset_of_list (?h # ?t)) \<equiv> fold min ?t ?h
### Code generator: dropping subsumed code equation
### fMax (fset_of_list (?a # ?as)) \<equiv> fold max ?as ?a
### Code generator: dropping subsumed code equation
### fMax (fset_of_list (?h # ?t)) \<equiv> last (nativeSort (?h # ?t))
### Code generator: dropping subsumed code equation
### fMin (fset_of_list (?h # ?t)) \<equiv> hd (nativeSort (?h # ?t))
### theory "Extended_Finite_State_Machine_Inference.Code_Target_FSet"
### 0.207s elapsed time, 0.892s cpu time, 0.000s GC time
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "Extended_Finite_State_Machine_Inference.Group_By"
### 0.261s elapsed time, 1.112s cpu time, 0.000s GC time
Found termination order: "(\<lambda>p. size (fst (snd p))) <*mlex*> {}"
### Code generator: dropping subsumed code equation
### [?i..<?j] \<equiv> if ?i < ?j then ?i # [Suc ?i..<?j] else []
### theory "Extended_Finite_State_Machine_Inference.Subsumption"
### 0.248s elapsed time, 0.996s cpu time, 0.000s GC time
Loading theory "Extended_Finite_State_Machine_Inference.Inference"
Loading theory "Extended_Finite_State_Machine_Inference.Drinks_Subsumption"
### Legacy feature! Old-style {* verbatim *} token -- use \<open>cartouche\<close> instead (line 1 of "$AFP/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy")
### Legacy feature! Old-style {* verbatim *} token -- use \<open>cartouche\<close> instead (line 2 of "$AFP/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy")
### theory "Extended_Finite_State_Machine_Inference.Code_Target_List"
### 0.421s elapsed time, 1.752s cpu time, 0.000s GC time
### theory "Extended_Finite_State_Machine_Inference.Drinks_Subsumption"
### 0.223s elapsed time, 0.892s cpu time, 0.000s GC time
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd (snd p)))
         (snd (snd (snd p)))) <*mlex*>
   {}"
*** Failed to apply proof method (line 77 of "$AFP/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy"):
*** goal (1 subgoal):
***  1. \<And>b. \<lbrakk>obtains 1 c
***           {|((0, 1), select), ((1, 1), vend_nothing), ((1, 2), coin),
***             ((2, 2), coin), ((2, 2), vend_fail), ((2, 3), vend)|}
***           0 <> t \<Longrightarrow>
***          c $ 2 = Some (Num 0);
***          a = (Label select, b); can_take_transition select b <>;
***          obtains 1 c
***           {|((0, 1), select), ((1, 1), vend_nothing), ((1, 2), coin),
***             ((2, 2), coin), ((2, 2), vend_fail), ((2, 3), vend)|}
***           1 (evaluate_updates select b <>) t\<rbrakk>
***         \<Longrightarrow> c $ 2 = Some (Num 0)
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd p)) (fst p)) <*mlex*> {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd (snd p))) (fst p)) <*mlex*> {}"
### theory "Extended_Finite_State_Machine_Inference.Inference"
### 5.277s elapsed time, 19.980s cpu time, 1.080s GC time
Loading theory "Extended_Finite_State_Machine_Inference.Distinguishing_Guards"
Loading theory "Extended_Finite_State_Machine_Inference.EFSM_Dot"
Loading theory "Extended_Finite_State_Machine_Inference.Increment_Reset"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "size <*mlex*> {}"
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
Loading theory "Extended_Finite_State_Machine_Inference.Least_Upper_Bound"
Found termination order: "size <*mlex*> {}"
Found termination order: "{}"
Found termination order: "size <*mlex*> {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
### theory "Extended_Finite_State_Machine_Inference.Increment_Reset"
### 1.801s elapsed time, 7.344s cpu time, 0.456s GC time
Loading theory "Extended_Finite_State_Machine_Inference.Same_Register"
### theory "Extended_Finite_State_Machine_Inference.EFSM_Dot"
### 2.093s elapsed time, 8.524s cpu time, 0.456s GC time
Loading theory "Extended_Finite_State_Machine_Inference.efsm2sal"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size (snd p)) (snd (snd p))) <*mlex*> {}"
Found termination order: "{}"
### theory "Extended_Finite_State_Machine_Inference.Same_Register"
### 0.548s elapsed time, 2.200s cpu time, 0.000s GC time
Loading theory "Extended_Finite_State_Machine_Inference.PTA_Generalisation"
Found termination order: "(\<lambda>p. size_list size (snd (snd p))) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd (snd p))) (fst p)) <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
### theory "Extended_Finite_State_Machine_Inference.Distinguishing_Guards"
### 2.700s elapsed time, 10.960s cpu time, 0.456s GC time
Loading theory "Extended_Finite_State_Machine_Inference.SelectionStrategies"
### theory "Extended_Finite_State_Machine_Inference.SelectionStrategies"
### 0.132s elapsed time, 0.536s cpu time, 0.000s GC time
Loading theory "Extended_Finite_State_Machine_Inference.Store_Reuse"
Found termination order: "size <*mlex*> {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "(\<lambda>p. size_list size (snd (snd p))) <*mlex*> {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd (snd p)))
         (snd (snd (snd p)))) <*mlex*>
   {}"
Found termination order:
  "(\<lambda>p. size_list (size_list (\<lambda>p. size_list size (fst (snd p))))
         (snd p)) <*mlex*>
   {}"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
Found termination order: "{}"
### theory "Extended_Finite_State_Machine_Inference.efsm2sal"
### 2.237s elapsed time, 8.912s cpu time, 0.636s GC time
Loading theory "Extended_Finite_State_Machine_Inference.Weak_Subsumption"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size (snd (snd (snd p)))) (snd p)) <*mlex*> {}"
Found termination order: "{}"
### theory "Extended_Finite_State_Machine_Inference.Store_Reuse"
### 1.718s elapsed time, 6.808s cpu time, 0.636s GC time
Loading theory "Extended_Finite_State_Machine_Inference.Store_Reuse_Subsumption"
Found termination order: "{}"
### theory "Extended_Finite_State_Machine_Inference.Weak_Subsumption"
### 0.344s elapsed time, 1.368s cpu time, 0.000s GC time
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd (snd p)))
         (fst (snd (snd (snd (snd p)))))) <*mlex*>
   {}"
### theory "Extended_Finite_State_Machine_Inference.Store_Reuse_Subsumption"
### 1.904s elapsed time, 6.556s cpu time, 4.200s GC time
Found termination order: "(\<lambda>p. size_list size (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size_list size (snd p)) <*mlex*> {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd (snd p))) (fst p)) <*mlex*> {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd (snd p)))
         (fst (snd (snd (snd p))))) <*mlex*>
   {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (fst (snd (snd (snd (snd p))))))
         (snd p)) <*mlex*>
   {}"
Found termination order: "{}"
### theory "Extended_Finite_State_Machine_Inference.Least_Upper_Bound"
### 17.377s elapsed time, 66.848s cpu time, 6.292s GC time
*** Excessive subgoal parameter specification (line 707 of "$AFP/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy")
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (fst (snd (snd (snd (snd p))))))
         (fst (snd p))) <*mlex*>
   {}"
Found termination order:
  "(\<lambda>p. size_list (size_list (\<lambda>p. size_list size (fst p))) (fst p)) <*mlex*>
   {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_option (\<lambda>p. size (fst p)) (snd p))
         (fst (snd (snd (snd p))))) <*mlex*>
   {}"
Found termination order: "size_list (\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size (snd p)) (fst p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd (snd p))) (fst (snd p))) <*mlex*>
   {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (snd (snd p))) (fst (snd p))) <*mlex*>
   {}"
Found termination order: "(\<lambda>p. length (snd (snd p))) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size_list size (fst p)) (fst (snd p))) <*mlex*> {}"
### theory "Extended_Finite_State_Machine_Inference.PTA_Generalisation"
### 28.247s elapsed time, 89.736s cpu time, 8.096s GC time
Loading theory "Extended_Finite_State_Machine_Inference.Code_Generation"
Found termination order: "{}"
*** Failed to apply proof method (line 75 of "$AFP/Extended_Finite_State_Machine_Inference/Code_Generation.thy"):
*** goal (2 subgoals):
***  1. \<And>v' l' l a.
***        \<lbrakk>l' \<notin> set l; s v = Some a\<rbrakk>
***        \<Longrightarrow> \<not>? (\<not>? (case s v' of None \<Rightarrow> invalid
***                   | Some vv \<Rightarrow> if vv \<in> set l then true else false) \<or>?
***                  (case s v' of None \<Rightarrow> invalid
***                   | Some vv \<Rightarrow> if vv \<in> set l then true else false)) \<or>?
***              (\<not>? value_eq (s v') (Some l') \<or>? value_eq (s v') (Some l')) \<noteq>
***           true
***  2. \<And>v l l'.
***        set l \<inter> set l' = {} \<Longrightarrow>
***        \<not>? (\<not>? (case s v of None \<Rightarrow> invalid
***                | Some vv \<Rightarrow> if vv \<in> set l' then true else false) \<or>?
***               (case s v of None \<Rightarrow> invalid
***                | Some vv \<Rightarrow> if vv \<in> set l' then true else false)) \<or>?
***           (\<not>? (case s v of None \<Rightarrow> invalid
***                | Some vv \<Rightarrow> if vv \<in> set l then true else false) \<or>?
***               (case s v of None \<Rightarrow> invalid
***                | Some vv \<Rightarrow> if vv \<in> set l then true else false)) \<noteq>
***        true
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "(\<lambda>p. size_list size (snd p)) <*mlex*> {}"
Found termination order: "{}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size (snd p)) (fst p)) <*mlex*> {}"
Found termination order: "size_list (\<lambda>p. size (snd p)) <*mlex*> {}"
See theory exports
### theory "Extended_Finite_State_Machine_Inference.Code_Generation"
### 19.239s elapsed time, 27.300s cpu time, 1.056s GC time
*** Failed to apply proof method (line 75 of "$AFP/Extended_Finite_State_Machine_Inference/Code_Generation.thy"):
*** goal (2 subgoals):
***  1. ⋀v' l' l a.
***        ⟦l' ∉ set l; s v = Some a⟧
***        ⟹ ¬? (¬? (case s v' of None ⇒ invalid
***                   | Some vv ⇒ if vv ∈ set l then true else false) ∨?
***                  (case s v' of None ⇒ invalid
***                   | Some vv ⇒ if vv ∈ set l then true else false)) ∨?
***              (¬? value_eq (s v') (Some l') ∨? value_eq (s v') (Some l')) ≠
***           true
***  2. ⋀v l l'.
***        set l ∩ set l' = {} ⟹
***        ¬? (¬? (case s v of None ⇒ invalid
***                | Some vv ⇒ if vv ∈ set l' then true else false) ∨?
***               (case s v of None ⇒ invalid
***                | Some vv ⇒ if vv ∈ set l' then true else false)) ∨?
***           (¬? (case s v of None ⇒ invalid
***                | Some vv ⇒ if vv ∈ set l then true else false) ∨?
***               (case s v of None ⇒ invalid
***                | Some vv ⇒ if vv ∈ set l then true else false)) ≠
***        true
*** At command "apply" (line 75 of "$AFP/Extended_Finite_State_Machine_Inference/Code_Generation.thy")
*** Excessive subgoal parameter specification (line 707 of "$AFP/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy")
*** At command "subgoal" (line 707 of "$AFP/Extended_Finite_State_Machine_Inference/heuristics/Least_Upper_Bound.thy")
*** Failed to apply proof method (line 77 of "$AFP/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy"):
*** goal (1 subgoal):
***  1. ⋀b. ⟦obtains 1 c
***           {|((0, 1), select), ((1, 1), vend_nothing), ((1, 2), coin),
***             ((2, 2), coin), ((2, 2), vend_fail), ((2, 3), vend)|}
***           0 <> t ⟹
***          c $ 2 = Some (Num 0);
***          a = (Label select, b); can_take_transition select b <>;
***          obtains 1 c
***           {|((0, 1), select), ((1, 1), vend_nothing), ((1, 2), coin),
***             ((2, 2), coin), ((2, 2), vend_fail), ((2, 3), vend)|}
***           1 (evaluate_updates select b <>) t⟧
***         ⟹ c $ 2 = Some (Num 0)
*** At command "apply" (line 77 of "$AFP/Extended_Finite_State_Machine_Inference/examples/Drinks_Subsumption.thy")