[SAL] --hide-locals

[swarup.mohalik at gm.com]

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/c0eea8c3/attachment.html