Email Gateway (Aug 18 2022 at 16:24): Email Gateway (Aug 18 2022 at 16:24):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hello,
want to use the statespace construct to model state spaces and i have
some questions:
0) is there some reference to statespace which might answer my
questions? until now i only have "State Spaces - The Locale Way" and
in there i could not find the answers to the following questions. (and
i found StateSpaceEx.thy which has similar examples)
1) before, i tried to model the statespace as a record. I defined
operational semantics of the type "record => instruction => record =>
bool" to have a function that indicates, whether the transition from
one state to another via an instruction is allowed. How can I do this
with statespaces, as they are not a variable type?
2) is there a way to instantiate such a statespace? Or is there no
need to? i'm still thinking in terms of records or functions, whose
variables could be updated bit by bit, but maybe
this just not the way statespaces are meant to be.
3) i played around with the variable renaming of statespaces. here's my example
statespace A = a::nat
statespace B = A + b::nat
statespace C = B[a=z] --- does not work
so my perception is, that i can only rename variables, that were
introduced in the named statespace, not in its parents.
why is it like this? is there some conceptual meaning?
thanks in advance
best regards
Nils
Email Gateway (Aug 18 2022 at 16:24):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hello,
want to use the statespace construct to model state spaces and i have
some questions:
0) is there some reference to statespace which might answer my
questions? until now i only have "State Spaces - The Locale Way" and
in there i could not find the answers to the following questions. (and
i found StateSpaceEx.thy which has similar examples)
1) before, i tried to model the statespace as a record. I defined
operational semantics of the type "record => instruction => record =>
bool" to have a function that indicates, whether the transition from
one state to another via an instruction is allowed. How can I do this
with statespaces, as they are not a variable type?
2) is there a way to instantiate such a statespace? Or is there no
need to? i'm still thinking in terms of records or functions, whose
variables could be updated bit by bit, but maybe
this just not the way statespaces are meant to be.
3) i played around with the variable renaming of statespaces. here's my example
statespace A = a::nat
statespace B = A + b::nat
statespace C = B[a=z] --- does not work
so my perception is, that i can only rename variables, that were
introduced in the named statespace, not in its parents.
why is it like this? is there some conceptual meaning?
thanks in advance
best regards
Nils
Email Gateway (Aug 18 2022 at 16:25):From: Norbert Schirmer <schirmer@in.tum.de>
Hello Nils,
On 08.11.2010, at 21:19, Nils Jähnig wrote:
Hello,
want to use the statespace construct to model state spaces and i have
some questions:0) is there some reference to statespace which might answer my
questions? until now i only have "State Spaces - The Locale Way" and
in there i could not find the answers to the following questions. (and
i found StateSpaceEx.thy which has similar examples)
I thought everything is said in that paper ;)
1) before, i tried to model the statespace as a record. I defined
operational semantics of the type "record => instruction => record =>
bool" to have a function that indicates, whether the transition from
one state to another via an instruction is allowed. How can I do this
with statespaces, as they are not a variable type?
As a statespace is just a locale, you
can define the function in the context of the statespace / locale using the "local-theory" concepts of Isabelle e.g.:
statespace state = ...
context state
begin
fun myfun
where
"myfun s = use s with selectors and updates here"
end
2) is there a way to instantiate such a statespace? Or is there no
need to? i'm still thinking in terms of records or functions, whose
variables could be updated bit by bit, but maybe
this just not the way statespaces are meant to be.
Yes by the standard means of locale instantiation.
There is currently not more automation.
For example you can define a record with all the fields, then instantiate the statespace-locale which leaves you with the obligation to proof that the record selector / update functions fulfill the locale assumptions, which they should.
3) i played around with the variable renaming of statespaces. here's my example
statespace A = a::nat
statespace B = A + b::nat
statespace C = B[a=z] --- does not workThis seems to be a bug or missing feature, but no conceptual thing.
Hope this helps.
Norbert
Last updated: Nov 21 2024 at 12:39 UTC