Theory Example_BLP

theory Example_BLP
imports TopoS_Library
begin

definition BLPexample1::"bool" where
  "BLPexample1 ≡ (nm_eval SINVAR_LIB_BLPbasic) fabNet ⦇ node_properties = [''PresenceSensor'' ↦ 2, 
                                                  ''Webcam'' ↦ 3, 
                                                  ''SensorSink'' ↦ 3,
                                                  ''Statistics'' ↦ 3] ⦈"
definition BLPexample3::"(string × string) list list" where
  "BLPexample3 ≡ (nm_offending_flows SINVAR_LIB_BLPbasic) fabNet ((nm_node_props SINVAR_LIB_BLPbasic) sensorProps_NMParams_try3)"

value "BLPexample1"
value "BLPexample3"


end