Email Gateway (May 10 2023 at 09:53): Email Gateway (May 10 2023 at 09:53):From: guilhermegfsilva@gmail.com
I'm trying to use the export command to generate code based on a simulation of
a state machine defined within a locale, where transitions between states
occur based on certain events. To do the code export from within a locale, I
believe I need to use the interpretation command to define some state machine
based on said locale. Here is my code so far:
theory SimpleStateMachine
imports Main
begin
locale StateMachine =
fixes
states :: "'state
set" (* set of states that
make up the machine *)
and evs :: "'ev set" (*
set of events *)
and initial :: "'state ⇒ bool" (*
predicate determining whether a state is the initial state *)
and stateTrans :: "'inE ⇒ ('state ⇒ 'state ⇒ bool)" (* predicate
defining transitions between states according to which events happen *)
begin
inductive reachable:: "'state ⇒ bool" where (* inductive
definition of whether a state is reachable *)
base: "initial x ⟹ reachable x" |
step: "(∃ y i. (reachable y ∧
stateTrans i x y)) ⟹ reachable x"
global_interpretation interp_1: StateMachine "states" "events" "(λ x . True)"
"(λ i x y . True)" (* this is a simplified definition assuming that
every state is initial and every transition is valid *)
defines reachable_def = interp_1.reachable
(* incomplete, see point #3 below *)
export_code
reachable_def
in Haskell module_name simple_haskell_3
What I would like to know is how to:
Define a set of arbitrary states (e.g. "a, b, c") and events (e.g. "i1,
i2") in my interpretation.
Define the interpretation of the "initial" and "stateTrans" functions of
the locale so that only some of the states (e.g. only "a") have the value of
the initial predicate be True and that the proper transitions between states
are defined (e.g. stateTrans has the True value for the parameters "i1 a b",
indicating that event i1 causes a transition from state a to state b).
Most importantly, how to specify the necessary proof in my interpretation
with the "defines" command so that export can have the required code equations
for "reachable_def". I believe I need to use "defines ___ by" followed by a
set of proof tactics, but how can I know what the necessary tactics are? If
there are any tutorials of how to do interpretations like this that provide
examples, that would be very helpful.
Thanks!
Email Gateway (May 11 2023 at 08:28):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi,
[…]
If
there are any tutorials of how to do interpretations like this that provide
examples, that would be very helpful.
the Tutorial on Code Generation
<https://isabelle.in.tum.de/dist/Isabelle2022/doc/codegen.pdf> contains
some basic examples.
It is difficult to tell on the spot whether an how these relate to your
issue(s). If the examples are not instructive, just come back to the
mailing list.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Last updated: Apr 24 2024 at 08:20 UTC