Theory Impl_List_Playground

theory Impl_List_Playground
imports "../TopoS_Impl"
begin


text‹The executbale models and the composition theory. We can build examples here›


definition testGraph :: "string list_graph" where
  "testGraph ≡ ⦇ nodesL = [''Master'', ''Slave1'', ''Slave2'', ''other1'', ''other2''], 
                 edgesL = [(''Master'', ''Slave1'')] ⦈"

lemma "wf_list_graph testGraph" by eval

definition req1 ::"(string SecurityInvariant)" where
  "req1 ≡ new_configured_list_SecurityInvariant SINVAR_SecGwExt_impl.SINVAR_LIB_PolEnforcePointExtended ⦇ 
      node_properties = [''Master'' ↦ PolEnforcePoint,
                         ''Slave1'' ↦ DomainMember,
                         ''Slave2'' ↦ DomainMember]
      ⦈ ''req1''"


definition "req2 ≡ new_configured_list_SecurityInvariant SINVAR_NoRefl_impl.SINVAR_LIB_NoRefl ⦇ 
      node_properties = [''Master'' ↦ Refl,
                         ''other1'' ↦ Refl,
                         ''other2'' ↦ Refl]
      ⦈ ''req2''"

definition "reqs = [req1, req2]"


definition "max_network = generate_valid_topology reqs 
      ⦇nodesL = nodesL testGraph, edgesL = List.product (nodesL testGraph) (nodesL testGraph) ⦈"

value "max_network"

ML‹
visualize_graph @{context} @{term "reqs"} @{term "max_network"};
›

end