|
From: Joe H. <joe...@co...> - 2004-06-11 15:27:39
|
On Fri, 11 Jun 2004, Radu Grigore wrote:
> I try to use the PSL example from HOL to generate checkers for
> properties in the "simple subset". The HOL version is from CVS,
> 7Jun.
>
> As far as I can tell the standalone pslcheck needs a path w and a
> PSL property p and it evaluates "w |= p", using definitions of |=
> and various other operators. This doesn't generate any checker
> so.
That's correct. pslcheck takes a trace and a PSL formula, and
evaluates whether the formula is true for the trace.
> There is another file, focs-example in the executable-semantics
> for 1.01, that illustrates creating checkers for SEREs. I am
> unable to use the techniques illustrated there to generate
> checkers for formulas as simple as "{a} |-> {b}". (formula "a"
> works, sere "a;b" works, more complicated sere work). Here is
> what I do:
The problem is that neither weak nor strong implication is in
the HOL simple subset of PSL formulas, because the HOL checker
generator is currently a prototype that works by translating PSL
formulas to PSL SEREs, and that can't be done for implication. Here is
the logical definition of the HOL simple subset, from
1.01/ExecuteSemanticsScript.sml:
val simple_def = Define
`(simple (F_BOOL b) = boolean (F_BOOL b)) /\
(simple (F_NOT (F_NOT f)) = simple f) /\
(simple (F_NOT (F_AND (F_NOT (F_UNTIL (f,g)), h))) =
simple f /\ boolean g /\ (h = F_UNTIL (F_BOOL B_TRUE, F_NOT f))) /\
(simple (F_NOT (F_AND (f,g))) = simple (F_NOT f) /\ simple (F_NOT g)) /\
(simple (F_NOT f) = boolean f) /\
(simple (F_AND (f,g)) = simple f /\ simple g) /\
(simple (F_NEXT f) = simple f) /\
(simple (F_UNTIL _) = F) /\
(simple (F_SUFFIX_IMP (r,f)) = S_CLOCK_FREE r /\ simple f) /\
(simple (F_STRONG_IMP _) = F) /\
(simple (F_WEAK_IMP _) = F) /\
(simple (F_ABORT _) = F) /\
(simple (F_STRONG_CLOCK _) = F)`;
> val fl = ``F_WEAK_IMP (S_BOOL (B_PROP a),S_BOOL (B_PROP b))``;
> (**
> NOTE: I get this by running (FL "{a} |-> {b}") and then
> replace by hand "a" with a and "b" with b. Is there another
> way?
> *)
Not until we create a standalone tool, similar to pslcheck, for
generating checkers.
> val dfa = extract_dfa alph re;
> (**
> NOTE: This takes a LOT of time and
> eventually throws Out of memory.
> *)
Interesting. I would speculate that since you're out of the HOL simple
subsert, internal formulas have irreducible terms that don't normalize
and so the HOL evaluator goes into a loop.
Regards,
Joe
|