[SAL] --hide-locals

[Leonardo de Moura]

Hi,

The option --hide-locals only affects the "-- System Variables  
(assignments) --"
section.  The constraints section is used when the decision procedure  
failed
to produced a concrete counterexample, and returned a set constraints.
Last week, we updated the SAL 2.4 pre-release binaries. They use a new
decision procedure that is faster and produces concrete counterexamples.
The binaries can be downloaded at:

http://sal.csl.sri.com/pre-release.shtml

Cheers,
Leonardo

On Jun 21, 2006, at 3:07 AM, swarup.mohalik at gm.com wrote:

>
> Hello all,
> [SAL on cygwin on a windows XP.]
>
> The --hide-locals option does not seem to work.
>
> simp_leader : CONTEXT=
> BEGIN
>         State : TYPE = {on};
>
>         main[delta : REAL] : MODULE=
>         BEGIN
>                 LOCAL state     : State
>                 LOCAL acc,v1,v0 : REAL
>                 LOCAL gap       : REAL
>
>                 INITIALIZATION
>                         state = on;
>                 TRANSITION
>                 [state = on -->
>                         v1'  = v1 + acc * delta;
>                         v0'  = v0 + (acc + v1 - v0) * delta;
>                         gap' = gap + (v1 - v0)
>                 ]
>
>         END;
>
>
>         th3 : THEOREM main[1] |- (gap >= 0) AND (v1 <= v0) => G(gap  
> >= 0);
>
> END
>
> bash>sal-inf-bmc simp_leader th3 -v 0 --delta-path --hide-locals
>
> Counterexample:
> ========================
> Path
> ========================
> Step 0:
> --- System Variables (assignments) ---
> --- Constraints ---
> v0 >= v1;
> gap >= 0;
> ------------------------
> Step 1:
> --- System Variables (assignments) ---
> --- Constraints ---
> gap = -1 * PRE(v0) + PRE(v1) + PRE(gap);
> ba-pc!1 >= 0;
> v1 = PRE(acc) + PRE(v1);
> acc = PRE(acc);
> -1 + ba-pc!1 = 0;
> ba-pc!1 >= 1;
> ba-pc!1 <= 2;
> v0 = PRE(acc) + PRE(v1);
> gap < 0;
> ------------------------
> Step 2:
> --- System Variables (assignments) ---
> --- Constraints ---
> v0 = PRE(acc) + PRE(v1);
> acc = PRE(acc);
> gap = -1 * PRE(v0) + PRE(v1) + PRE(gap);
> v1 = PRE(acc) + PRE(v1);
>
>
> Please look into this.
> -----------------------
> Swarup Mohalik

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/sal/attachments/20060621/f7375684/attachment.html