theory LTS_Parser
imports
Auxx.Xmlt2
IA_Instance
begin
hide_const (open) name
context
fixes atom_parser :: "('f,'a,'t) exp formula xmlt2"
begin
partial_function (sum_bot) formula_parser :: "('f,'a,'t) exp formula xmlt2" where
[code]: "formula_parser x = (
XMLdo (STR ''disjunction'') {
fs ←* formula_parser; xml_return (Disjunction fs)
} XMLor XMLdo (STR ''conjunction'') {
fs ←* formula_parser; xml_return (Conjunction fs)
} XMLor atom_parser) x"
end
context
fixes location_parser :: "'l xmlt2"
and trans_parser :: "'tr xmlt2"
and tatom_parser :: "('f,'v trans_var,'t) exp formula xmlt2"
begin
definition transition_parser :: "('tr × ('f,'v,'t,'l) transition_rule) xmlt2" where
"transition_parser ≡ XMLdo (STR ''transition'') {
tr ← trans_parser;
l ← xml_do (STR ''source'') (xml_take location_parser xml_return);
r ← xml_do (STR ''target'') (xml_take location_parser xml_return);
φ ← xml_do (STR ''formula'') (xml_take (formula_parser tatom_parser) xml_return);
xml_return (tr, Transition l r φ)
}"
definition lts_parser :: "ltag ⇒ ('f,'v,'t,'l,'tr) lts_impl xmlt2" where
"lts_parser tag ≡ XMLdo tag {
i ← xml_do (STR ''initial'') (xml_take_many 1 ∞ location_parser xml_return);
t ←* transition_parser;
xml_return (Lts_Impl i t [])
}"
definition "safety_input_parser ≡
XMLdo (STR ''ltsSafetyInput'') {
lts ← lts_parser (STR ''lts'');
err ← xml_do (STR ''error'') (xml_take_many 1 ∞ location_parser xml_return);
xml_return (lts,err)
}"
end
context
fixes art_node_id_parser :: "ltag ⇒ 'n xmlt2"
and location_parser :: "'l xmlt2"
and trans_parser :: "'tr xmlt2"
and atom_parser :: "('f,'v,'t) exp formula xmlt2"
and hint_parser :: "'h :: default xmlt2"
begin
definition formula_pos_parser :: "nat xmlt2" where [code]:
"formula_pos_parser =
XMLdo (STR ''conclusion'') {xml_return 0}
XMLor XMLdo (STR ''assertion'') {xml_return 2}
XMLor XMLdo (STR ''transition'') {xml_return 3}
XMLor XMLdo (STR ''targetAssertion'') {xml_return 4}"
partial_function (sum_bot) hints_parser :: "'h hint xmlt2" where
[code]: "hints_parser xml = (
XMLdo (STR ''auto'') {
xml_return default
} XMLor XMLdo (STR ''distribute'') {
pos ← formula_pos_parser;
hints ←* hints_parser;
xml_return (hint.Distribute pos hints)
} XMLor XMLdo (STR ''erase'') {
pos ← formula_pos_parser;
hint ← hints_parser;
xml_return (hint.Erase pos hint)
} XMLor XMLdo (STR ''lexWeak'') {
hints ←* hints_parser;
xml_return (hint.LexWeak hints)
} XMLor XMLdo (STR ''lexStrict'') {
hints ←* hints_parser;
xml_return (hint.LexStrict hints)
} XMLor
xml_change hint_parser (xml_return ∘ hint.Base)
) xml"
definition art_node_parser :: "(('f, 'v, 't, 'l, 'n, 'tr, 'h hint) art_node_impl × 'n list) xmlt2" where
"art_node_parser ≡ XMLdo (STR ''node'') {
init ←[False] (xml_do (STR ''initial'') (xml_return True));
nodeId ← art_node_id_parser (STR ''nodeId'');
invariant ← xml_do (STR ''invariant'') (xml_take (formula_parser atom_parser) xml_return);
location ← xml_do (STR ''location'') (xml_take location_parser xml_return);
edges ← XMLdo (STR ''children'') {
chs ←*
XMLdo (STR ''child'') {
tr ← trans_parser;
n ← art_node_id_parser (STR ''nodeId'');
h ←[default] (xml_do (STR ''hints'') (xml_take hints_parser xml_return));
xml_return (tr, n, h)
};
xml_return (Children_Edge chs)
} XMLor XMLdo (STR ''coverEdge'') {
n ← art_node_id_parser (STR ''nodeId'');
h ←[default] xml_do (STR ''hints'') (xml_take hints_parser xml_return);
xml_return (Cover_Edge n h)
};
xml_return (Art_Node nodeId invariant location edges, if init then [nodeId] else [])
}"
definition art_parser :: "(('f, 'v, 't, 'l, 'n, 'tr, 'h hint) art_impl) xmlt2" where
"art_parser ≡ XMLdo (STR ''impact'') {
init ←[[]] xml_change (art_node_id_parser (STR ''initial'')) (λx. xml_return [x]);
pairs ← xml_do (STR ''nodes'') (xml_take_many 0 ∞ art_node_parser xml_return);
let nodes = map fst pairs;
let inits = init @ concat (map snd pairs);
xml_return ⦇ art_impl.initial_nodes = inits, nodes = nodes ⦈
}"
end
context
fixes location_parser :: "'l xmlt2"
and trans_parser :: "'tr xmlt2"
and atom_parser :: "('f,'v,'t) exp formula xmlt2"
and hint_parser :: "'h :: default xmlt2"
begin
type_synonym art_node_id = string
abbreviation art where "art ≡ art_parser xml_text location_parser trans_parser atom_parser hint_parser"
definition "invariant_proof_parser I ≡
xml_change art (λ prf. xml_return (Impact I prf))"
definition invariant_parser :: "('l × ('f,'v,'t) exp formula) xmlt2" where
"invariant_parser ≡ XMLdo (STR ''invariant'') {
l ← xml_do (STR ''location'') (xml_take location_parser xml_return);
φ ← xml_do (STR ''formula'') (xml_take (formula_parser atom_parser) xml_return);
xml_return (l,φ)
}"
definition invariants_parser :: "('l × ('f,'v,'t) exp formula)list xmlt2" where
"invariants_parser ≡ xml_do (STR ''invariants'') (xml_take_many 0 ∞ invariant_parser xml_return)"
definition safety_proof_parser :: "('f,'v,'t,'l,string,'tr,'h) safety_proof xmlt2" where
"safety_proof_parser ≡ XMLdo (STR ''safetyViaInvariants'') {
I ← invariants_parser;
p ← invariant_proof_parser I;
xml_return (safety_proof.Invariant_Assertion p safety_proof.Trivial)
}"
end
fun cut_points_to_transitions :: "_ ⇒ _ ⇒ ('f,'v,'t,'l sharp,'tr sharp) transitions_impl" where
"cut_points_to_transitions ts [] = ts"
| "cut_points_to_transitions ts ((l,tr,φ)#cps) =
cut_points_to_transitions ((Flat tr, Transition (Flat l) (Sharp l) φ)#ts) cps"
context
fixes location_id_parser :: "ltag ⇒ 'l xmlt2"
and trans_id_parser :: "ltag ⇒ 'tr xmlt2"
and exp_parser :: "('f,'v,'t) exp xmlt2"
and atom_parser :: "('f,'v,'t) exp formula xmlt2"
and tatom_parser :: "('f,'v trans_var,'t) exp formula xmlt2"
and variable_parser :: "'v xmlt2"
and trans_var_parser :: "'v trans_var xmlt2"
and hint_parser :: "'h :: default xmlt2"
and type_parser :: "'t xmlt2"
and dom_type :: "'t"
begin
definition "location_parser ≡ location_id_parser (STR ''locationId'')"
definition sharp_location_parser :: "'l sharp xmlt2" where
"sharp_location_parser ≡
(xml_change (location_id_parser (STR ''locationDuplicate'')) (xml_return ∘ Sharp))
XMLor (xml_change (location_id_parser (STR ''locationId'')) (xml_return ∘ Flat))"
abbreviation "tformula ≡ formula_parser tatom_parser"
context
fixes trans_parser :: "'trr xmlt2"
begin
abbreviation "lts ≡ lts_parser sharp_location_parser trans_parser tatom_parser"
abbreviation "transition ≡ transition_parser sharp_location_parser trans_parser tatom_parser"
abbreviation "invariant_proof ≡ invariant_proof_parser sharp_location_parser trans_parser atom_parser hint_parser"
abbreviation "invariants ≡ invariants_parser sharp_location_parser atom_parser"
partial_function (sum_bot) cooperation_proof_parser where [code]: "cooperation_proof_parser xs = (
xml_do (STR ''trivial'') (xml_return cooperation_proof.Trivial)
XMLor XMLdo (STR ''newInvariants'') {
i ← invariants;
p ← invariant_proof i;
cp ← cooperation_proof_parser;
xml_return (Invariants_Update p cp)
} XMLor XMLdo (STR ''transitionRemoval'') {
rs ← XMLdo (STR ''rankingFunctions'') {
pairs ←* XMLdo (STR ''rankingFunction'') {
l ← xml_do (STR ''location'') (xml_take sharp_location_parser xml_return);
es ← xml_do (STR ''expression'') (xml_take_many 1 ∞ exp_parser xml_return);
xml_return (l,es)
};
xml_return pairs};
bounds ← xml_do (STR ''bound'') (xml_take_many 0 ∞ exp_parser xml_return);
removed ← xml_do (STR ''remove'') (xml_take_many 0 ∞ trans_parser xml_return);
hinter ←[λx. default] XMLdo (STR ''hints'') {
pairs ←* XMLdo (STR ''hint'') {
tr ← trans_parser;
hint ←[default] hints_parser hint_parser;
xml_return (tr, hint)
};
xml_return (map_of_default default pairs)};
inner ← cooperation_proof_parser;
let rf = map_of_default [] rs;
xml_return (Transition_Removal (Transition_removal_info rf removed dom_type bounds hinter) inner)
} XMLor XMLdo (STR ''locationAddition'') {
tr ← transition;
prof ← cooperation_proof_parser;
let (tr_id,tau) = tr;
xml_return (Location_Addition (Location_Addition_Info (source tau) (target tau) tr_id tau) prof)
} XMLor XMLdo (STR ''freshVariableAddition'') {
x1 ← variable_parser;
x2 ← type_parser;
x3 ← XMLdo (STR ''additionalFormulas'') {
pairs ←* XMLdo (STR ''additionalFormula'') {
tr ← trans_parser;
φ ← tformula;
xml_return (tr,φ)
};
xml_return pairs
};
prof ← cooperation_proof_parser;
xml_return (Fresh_Variable_Addition (Fresh_Variable_Addition_Info x1 x2 x3) prof)
} XMLor XMLdo (STR ''cutTransitionSplit'') {
ps ←* (XMLdo (STR ''cutTransitionsWithProof'') {
cuts ← xml_do (STR ''cutTransitions'') (xml_take_many 0 ∞ trans_parser xml_return);
prof ← cooperation_proof_parser;
xml_return (cuts,prof)});
xml_return (Cut_Transition_Split ps)
} XMLor XMLdo (STR ''sccDecomposition'') {
sccs ←* XMLdo (STR ''sccWithProof'') {
scc :: 'l sharp list ← xml_do (STR ''scc'') (xml_take_many 1 ∞ sharp_location_parser xml_return);
prof ← cooperation_proof_parser;
xml_return (scc,prof)};
xml_return (Scc_Decomp sccs)
}) xs"
end
definition "trans_id ≡ trans_id_parser (STR ''transitionId'')"
definition "sharp_trans_id ≡
xml_change (trans_id_parser (STR ''transitionDuplicate'')) (xml_return ∘ Sharp)
XMLor xml_change (trans_id_parser (STR ''transitionId'')) (xml_return ∘ Flat)"
definition "cutPoints_parser ≡ XMLdo (STR ''cutPoints'') {
tuples ←* XMLdo (STR ''cutPoint'') {
l ← location_id_parser (STR ''locationId'');
tr ← trans_id_parser (STR ''skipId'');
φ ← XMLdo (STR ''skipFormula'') {
ret ← tformula;
xml_return ret
};
xml_return (l,tr,φ)
};
xml_return (cut_points_to_transitions [] tuples)
}"
partial_function (sum_bot) termination_proof_parser where [code]: "termination_proof_parser xml = (
XMLdo (STR ''trivial'') {
xml_return termination_proof.Trivial
} XMLor XMLdo (STR ''newInvariants'') {
i ← invariants_parser location_parser atom_parser;
p ← invariant_proof_parser location_parser trans_id atom_parser hint_parser i;
cp ← termination_proof_parser;
xml_return (Invariants_Update_LTS p cp)
} XMLor XMLdo (STR ''switchToCooperationTermination'') {
cp ← cutPoints_parser;
p ← cooperation_proof_parser sharp_trans_id;
xml_return (termination_proof.Via_Cooperation [(cp,p)])
}
) xml"
end
type_synonym location_id = string
type_synonym transition_id = string
type_synonym variable_id = string
definition variable_parser :: "variable_id xmlt2" where
"variable_parser = xml_text (STR ''variableId'')"
definition trans_var_parser :: "variable_id trans_var xmlt2" where
"trans_var_parser =
XMLdo (STR ''post'') {v ← variable_parser; xml_return (Post v)}
XMLor XMLdo (STR ''aux'') {v ← variable_parser; xml_return (Intermediate v)}
XMLor xml_change variable_parser (xml_return ∘ Pre)"
definition "constant_parser ≡ xml_int (STR ''constant'')"
partial_function (sum_bot) exp_parser' :: "'a xmlt2 ⇒ 'a IA.exp xmlt2" where
[code]: "exp_parser' v xml = (
XMLdo (STR ''product'') {
exps ←* exp_parser' v;
xml_return (Fun (IA.ProdF (length exps)) exps)
} XMLor XMLdo (STR ''sum'') {
exps ←* exp_parser' v;
xml_return (Fun (IA.SumF (length exps)) exps)
} XMLor xml_change (xml_int (STR ''constant'')) (λi. xml_return (IA.const i))
XMLor xml_change v (λ x. xml_return (IA.var x))
) xml"
definition bexp_parser' :: "'a xmlt2 ⇒ 'a IA.formula xmlt2" where
"bexp_parser' v ≡
(let bexp_parser'' =
XMLdo (STR ''leq'') {
l ← exp_parser' v;
r ← exp_parser' v;
xml_return (Fun IA.LeF [l, r])
} XMLor XMLdo (STR ''less'') {
l ← exp_parser' v;
r ← exp_parser' v;
xml_return (Fun IA.LessF [l,r])
} XMLor XMLdo (STR ''eq'') {
l ← exp_parser' v;
r ← exp_parser' v;
xml_return (Fun IA.EqF [l,r])
} XMLor XMLdo (STR ''geq'') {
l ← exp_parser' v;
r ← exp_parser' v;
xml_return (Fun IA.LeF [r,l])
} XMLor XMLdo (STR ''greater'') {
l ← exp_parser' v;
r ← exp_parser' v;
xml_return (Fun IA.LessF [r,l])
}
in
XMLdo STR ''not'' {a ← bexp_parser''; xml_return (NegAtom a)}
XMLor xml_change bexp_parser'' (xml_return ∘ Atom))"
definition "exp_parser ≡ exp_parser' variable_parser"
definition "atom_parser ≡ xml_change (bexp_parser' variable_parser) xml_return"
definition "tatom_parser ≡ xml_change (bexp_parser' trans_var_parser) xml_return"
definition "atom_parser' = xml_change (bexp_parser' variable_parser) xml_return"
definition "tatom_parser' = xml_change (bexp_parser' trans_var_parser) xml_return"
definition valuation_parser :: "(string × string IA.exp) list xmlt2"
where
"valuation_parser = XMLdo (STR ''substitution'') {
list ←* XMLdo (STR ''substEntry'') {
var ← variable_parser;
expr ← exp_parser;
xml_return (var,expr)
};
xml_return list
}"
definition state_parser
where "state_parser ≡ XMLdo (STR ''state'') {
loc ← location_parser xml_text;
s ← valuation_parser;
xml_return (s, loc)
}"
definition hint_parser :: "hints xmlt2" where
"hint_parser ≡ XMLdo (STR ''linearCombination'') {
xs ←* xml_int (STR ''constant'');
xml_return (Hints xs)
}"
definition type_parser :: "IA.ty xmlt2" where
"type_parser ≡
XMLdo (STR ''int'') {xml_return IA.IntT} XMLor XMLdo (STR ''bool'') {xml_return IA.BoolT}"
definition "lts_input_parser ≡
lts_parser
(location_parser xml_text)
(trans_id xml_text) tatom_parser' (STR ''lts'')"
definition "lts_safety_input_parser ≡
safety_input_parser (location_parser xml_text) (trans_id xml_text) tatom_parser'"
definition "lts_termination_proof_parser ≡
termination_proof_parser
xml_text
xml_text
exp_parser atom_parser tatom_parser variable_parser hint_parser type_parser IA.IntT"
definition "lts_safety_proof_parser ≡
safety_proof_parser (location_parser xml_text) (trans_id xml_text) atom_parser hint_parser"
definition transition_step_parser where "transition_step_parser ≡
XMLdo (STR ''transitionStep'') {
src ← state_parser;
tid ← trans_id xml_text;
tgt ← state_parser;
xml_return (src, tid, tgt)
}"
definition transition_seq_parser
where
"transition_seq_parser name = XMLdo name {
list ←* transition_step_parser;
xml_return list
}"
definition nontermination_proof where "nontermination_proof ≡
XMLdo (STR ''equivalentState'') {
i ← location_parser xml_text;
stem ← transition_seq_parser (STR ''stem'');
loop ← transition_seq_parser (STR ''loop'');
xml_return (i, stem, loop)
}"
context
fixes location_parser :: "'l xmlt2"
and trans_parser :: "'tr xmlt2"
and trans_var_parser :: "'v trans_var xmlt2"
and tatom_parser :: "('f,'v trans_var,'t) Sorted_Algebra.exp Formula.formula xmlt2"
begin
definition "nontermination_input_parser ≡
XMLdo (STR ''nonterminationInput'') {
lts ← lts_parser location_parser trans_parser tatom_parser (STR ''lts'');
xml_return lts
}"
end
end