Theory efsm2sal

section‹Output to SAL›
text‹SAL is a framework for combining different tools for abstraction, program analysis, theorem
proving, and model checking. It is able to verify and refute properties of EFSMs phrased in LTL. In
\<^cite>‹"foster2019"›, it is proposed that a model checker be used to assist in checking the conditions
necessary for one transition to subsume another. In order to effect this, it is necessary to convert
the EFSM into a format that SAL can recognise. This theory file sets out the various definitions
needed to do this such that SAL can be used to check subsumption conditions when running the EFSM
inference tool generated by the code generator.›

theory efsm2sal
  imports "EFSM_Dot"
begin

definition replace :: "String.literal ⇒ String.literal ⇒ String.literal ⇒ String.literal" where
  "replace s old new = s"

code_printing constant replace ⇀ (Scala) "_.replaceAll(_, _)"

definition escape :: "String.literal ⇒ (String.literal × String.literal) list ⇒ String.literal" where
  "escape s replacements = fold (λ(old, new) s'. replace s' old new) replacements s"

definition "replacements = [
  (STR ''/'', STR ''_SOL__''),
  (STR 0x5C+STR 0x5C, STR ''_BSOL__''),
  (STR '' '', STR ''_SPACE__''),
  (STR 0x5C+STR ''('', STR ''_LPAR__''),
  (STR 0x5C+STR '')'', STR ''_RPAR__''),
  (STR 0x5C+STR ''.'', STR ''_PERIOD__''),
  (STR ''@'', STR ''_COMMAT__'')
]"

fun aexp2sal :: "vname aexp ⇒ String.literal" where
  "aexp2sal (L (Num n)) = STR ''Some(Num(''+ show_int n + STR ''))''"|
  "aexp2sal (L (value.Str n)) = STR ''Some(Str(String__''+ (if n = STR '''' then STR ''_EMPTY__'' else escape n replacements) + STR ''))''" |
  "aexp2sal (V (I i)) = STR ''Some(i('' + show_nat (i) + STR ''))''" |
  "aexp2sal (V (R r)) = STR ''r__'' + show_nat r" |
  "aexp2sal (Plus a1 a2) = STR ''value_plus(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
  "aexp2sal (Minus a1 a2) = STR ''value_minus(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
  "aexp2sal (Times a1 a2) = STR ''value_times(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''"

fun gexp2sal :: "vname gexp ⇒ String.literal" where
  "gexp2sal (Bc True) = STR ''True''" |
  "gexp2sal (Bc False) = STR ''False''" |
  "gexp2sal (Eq a1 a2) = STR ''value_eq('' + aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
  "gexp2sal (Gt a1 a2) = STR ''value_gt('' + aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
  "gexp2sal (In v l) = join (map (λl'.  STR ''gval(value_eq('' + aexp2sal (V v) + STR '', '' + aexp2sal (L l') + STR ''))'') l) STR '' OR ''" |
  "gexp2sal (Nor g1 g2) = STR ''NOT (gval('' + gexp2sal g1 + STR '') OR gval( '' + gexp2sal g2 + STR ''))''"

fun guards2sal :: "vname gexp list ⇒ String.literal" where
  "guards2sal [] = STR ''TRUE''" |
  "guards2sal G = join (map gexp2sal G) STR '' AND ''"

fun aexp2sal_num :: "vname aexp ⇒ nat ⇒ String.literal" where
  "aexp2sal_num (L (Num n)) _ = STR ''Some(Num(''+ show_int n + STR ''))''"|
  "aexp2sal_num (L (value.Str n)) _ = STR ''Some(Str(String__''+ (if n = STR '''' then STR ''_EMPTY__'' else escape n replacements) + STR ''))''" |
  "aexp2sal_num (V (vname.I i)) _ = STR ''Some(i('' + show_nat i + STR ''))''" |
  "aexp2sal_num (V (vname.R i)) m = STR ''r__'' + show_nat i + STR ''.'' + show_nat m" |
  "aexp2sal_num (Plus a1 a2) _ = STR ''value_plus(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
  "aexp2sal_num (Minus a1 a2) _ = STR ''value_minus(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
  "aexp2sal_num (Times a1 a2) _ = STR ''value_times(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''"

fun gexp2sal_num :: "vname gexp ⇒ nat ⇒ String.literal" where
  "gexp2sal_num (Bc True) _ = STR ''True''" |
  "gexp2sal_num (Bc False) _ = STR ''False''" |
  "gexp2sal_num (Eq a1 a2) m = STR ''gval(value_eq('' + aexp2sal_num a1 m + STR '', '' + aexp2sal_num a2 m + STR ''))''" |
  "gexp2sal_num (Gt a1 a2) m = STR ''gval(value_gt('' + aexp2sal_num a1 m + STR '', '' + aexp2sal_num a2 m + STR ''))''" |
  "gexp2sal_num (In v l) m = join (map (λl'.  STR ''gval(value_eq('' + aexp2sal_num (V v) m + STR '', '' + aexp2sal_num (L l') m + STR ''))'') l) STR '' OR ''" |
  "gexp2sal_num (Nor g1 g2) m = STR ''NOT ('' + gexp2sal_num g1 m + STR '' OR '' + gexp2sal_num g2 m + STR '')''"

fun guards2sal_num :: "vname gexp list ⇒ nat ⇒ String.literal" where
  "guards2sal_num [] _ = STR ''TRUE''" |
  "guards2sal_num G m = join (map (λg. gexp2sal_num g m) G) STR '' AND ''"

end