# Theory Test_Suite

section ‹Test Suites›
text ‹This theory introduces a predicate @{text "implies_completeness"} and proves that
any test suite satisfying this predicate is sufficient to check the reduction conformance
relation between two (possibly nondeterministic FSMs)›
theory Test_Suite
imports Helper_Algorithms Adaptive_Test_Case Traversal_Set
begin
subsection ‹Preliminary Definitions›
type_synonym ('a,'b,'c) preamble = "('a,'b,'c) fsm"
type_synonym ('a,'b,'c) traversal_path = "('a × 'b × 'c × 'a) list"
type_synonym ('a,'b,'c) separator = "('a,'b,'c) fsm"
text ‹A test suite contains of
1) a set of d-reachable states with their associated preambles
2) a map from d-reachable states to their associated m-traversal paths
3) a map from d-reachable states and associated m-traversal paths to the set of states to r-distinguish the targets of those paths from
4) a map from pairs of r-distinguishable states to a separator›