Theory CollectionBasedRTS

(* Title: RTS/Common/CollectionBasedRTS.thy *)
(* Author: Susannah Mansky, UIUC 2020 *)

section "Collection-based RTS"

theory CollectionBasedRTS
imports RTS_safe CollectionSemantics
begin

locale CollectionBasedRTS_base = RTS_safe + CollectionSemantics

text "General model for Regression Test Selection based on
 @{term CollectionSemantics}:"
locale CollectionBasedRTS = CollectionBasedRTS_base where
  small = "small :: 'prog ⇒ 'state ⇒ 'state set" and
  collect = "collect :: 'prog ⇒ 'state ⇒ 'state ⇒ 'coll" and
  out = "out :: 'prog ⇒ 'test ⇒ ('state × 'coll) set"
 for small collect out
+
 fixes
  make_test_prog :: "'prog ⇒ 'test ⇒ 'prog" and
  collect_start :: "'prog ⇒ 'coll"
 assumes
  out_cbig:
   "∃i. out P t = {(σ',coll'). ∃coll. (σ',coll) ∈ cbig (make_test_prog P t) i
                                                  ∧ coll' = combine coll (collect_start P) }"

context CollectionBasedRTS begin

end ― ‹ CollectionBasedRTS ›

end