Re: [Hol-info] psl example

[Joe H. <joe...@co...>]

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