Theory DBM_Examples

theory DBM_Examples
  imports 
    DBM_Operations_Impl_Refine 
    FW_More 
    Show.Show_Instances
begin

section ‹Examples›

no_notation Ref.update (‹_ := _› 62)

text ‹Let us represent the zone ‹y ≤ x ∧ x − y ≤ 2 ∧ y ≥ 1› as a DBM:›
definition test_dbm :: "int DBM'" where
  "test_dbm = ((((λ(i, j). Le 0)((1,2) := Le 2))((0, 2) := Le (-1)))((1, 0) := ∞))((2, 0) := ∞)"

― ‹Pretty-printing›
definition show_test_dbm where
  "show_test_dbm M = String.implode (
    show_dbm 2
      (λi. if i = 1 then ''x'' else if i = 2 then ''y'' else ''f'') show
      M
    )"

― ‹Pretty-printing›
value [code] "show_test_dbm test_dbm"

― ‹Canonical form›
value [code] "show_test_dbm (FW' test_dbm 2)"

― ‹Projection onto ‹x› axis›
value [code] "show_test_dbm (reset'_upd (FW' test_dbm 2) 2 [2] 0)"
― ‹Note that if \<^term>‹reset'_upd› is not applied to the canonical form, the result is incorrect:›
value [code] "show_test_dbm (reset'_upd test_dbm 2 [2] 0)"
― ‹In this case, we already obtained a new canonical form after reset:›
value [code] "show_test_dbm (FW' (reset'_upd (FW' test_dbm 2) 2 [2] 0) 2)"
― ‹Note that \<^term>‹FWI› can be used to restore the canonical form without running a full \<^term>‹FW'›.›

― ‹Relaxation, a.k.a computing the "future", or "letting time elapse":›
value [code] "show_test_dbm (up_canonical_upd (reset'_upd (FW' test_dbm 2) 2 [2] 0) 2)"
― ‹Note that \<^term>‹up_canonical_upd› always preservers canonical form.›

― ‹Intersection›
value [code] "show_test_dbm (FW' (And_upd 2
    (up_canonical_upd (reset'_upd (FW' test_dbm 2) 2 [2] 0) 2)
    ((λ(i, j). ∞)((1, 0):=Lt 1))) 2)"
― ‹Note that \<^term>‹up_canonical_upd› always preservers canonical form.›

― ‹Checking if DBM represents the empty zone›
value [code] "check_diag 2 (FW' (And_upd 2
    (up_canonical_upd (reset'_upd (FW' test_dbm 2) 2 [2] 0) 2)
    ((λ(i, j). ∞)((1, 0):=Lt 1))) 2)"

― ‹Instead of \<^term>‹λ(i, j). ∞› we could also have been using \<^term>‹unbounded_dbm›.›

end