[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Induction on FSA

Dear Cesar,

First of all, thanks for your reply.

I had seen already that slides set as part of the Nasa virtual machine
material. The project you linked me is very huge and I have quite some
difficulties into following it (there are so many files that I hardly
can find the beginning).

The problem is that my theory is very convoluted, and recursive
functions call other functions. I am now trying to prove them "step by
step", by defining the inner behavior as lemmas to be proved from the
inside out.

But still, I get stuck even in the simplest cases. For example, I have
a function defined as (t_Label_STAR_y is just a list of t_Label_y
elements, which is a datatype that can be either addMatrix_y or
removeMatrix_y, a disjoint union):

alfa(org: t_Strings, newAuth: finite_set[t_TripleString]):
	  IF empty?(newAuth) THEN
	      %Add the Auth
	      %Add the Belongs W.Bel(sub,org) <--> Y.Mat(sub, org, sk(sub,org))
		(# e1:= choose(newAuth)`e1, e2 := org, e3 :=
skolem_generator_belongs(choose(newAuth)`e1, org) #)
	      alfa_helper_joinCoalitionCons_w(org, rest(newAuth))))
MEASURE card(newAuth)

As you can see here, all I'm doing is appending addMatrix elements.
This means that the list is either empty or composed only of addMatrix

So I have tried to prove the lemma:

jc_help: LEMMA
(FORALL (sy: t_States_y, lw: t_Labels_w):
	joinCoalition_w?(lw) IMPLIES (FORALL (ly: t_Labels_y): alfa(sy,
lw)(ly) IMPLIES addMatrix_y?(ly))

And yet, if I use induct on lw I get stuck, after some trivial
passages, as I don't have anything left quantified and I start "going
down" in the recursion manually:

{-1}  list2set(cdr(cdr(alfa_helper_joinCoalitionCons_w(ORG, NEWAUTH))))
[1]   null?(alfa_helper_joinCoalitionCons_w(ORG, NEWAUTH))
{2}   null?(cdr(alfa_helper_joinCoalitionCons_w(ORG, NEWAUTH)))
[3]   addMatrix_y?(ly!1)

and on and on cdr(cdr(cdr( ...



2013/2/26 MUNOZ, CESAR  (LARC-D320) <cesar.a.munoz@xxxxxxxx>:
> Diego,
> The technique depends on what you want to prove and how you defined your
> recursive function. Please, take a look at this talk on recursion and
> induction in PVS.
> http://shemesh.larc.nasa.gov/PVSClass2012/pvsclass2012/lectures-printer/ind
> uction.pdf
> A concrete example, which deals with a state automaton, can be found here:
>   http://shemesh.larc.nasa.gov/people/cam/AirSTAR/
> Hope that this helps,
> Cesar
> --
> Cesar A. Munoz                             NASA Langley Research Center
> Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
> http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
> Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234
> On 2/24/13 10:04 AM, "Diego Martinoia" <diego.martinoia@xxxxxxxxx> wrote:
>>Dear all,
>>I'm quite new to PVS, and I was wondering if anyone could help me:
>>I am working on a theory that involves simulating finite state
>>automaton, and I have to prove a lemma in the form:
>>s1 = terminal ( s2, lx )
>>where s1 and s2 are states of the automaton, lx is a list of inputs
>>(the labels on the automaton arches) and terminal is a recursive
>>function defined as:
>>terminal(s, lx) =
>>IF null?(lx) THEN s
>>terminal (next (s, car(lx)) , cdr(lx))
>>where next is the single step function of the automaton, car and cdr
>>are the list accessors for the head and the rest of the list.
>>Unfortunately, I can't figure out which commands allow me to deal with
>>this kind of structure. I have tried launching a
>>induct-and-simplify "lx"
>>command, as well as similar form involving using the name and
>>generalize-skolem-constants commands to have more possible argument
>>for the induction rules, but I always fail.
>>Anyone has any suggestions on the matter?
>>Diego Martinoia