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

Re: pb with measure in a recursive function



Hi David,

Could you send enough of the spec so that I can try and typecheck this
myself?  I expect the error message is hiding the real problem.

Thanks,
Sam Owre


> From:    David <doups@netcourrier.com>
> Subject: pb with measure in a recursive function
> Date:    Mon,  7 Jul 2003 11:36:32 CEST
> To:      pvs-help@csl.sri.com
> 
> hi, i have this recursive function :
> 
> parbeh(b : behaviour, st : stock ) : recursive behaviour  = 
> 		if ( tyBeh(b)="replicate") then parbeh(behReplicate(b), ( let  a = (#typB:="replicate", be := behReplicate(b), ensCon:=emptyset, ensVar:=emptyset, ensAction := emptyset #) in parbeh(done,add(a,st))))
> 		else 
> 			if (tyBeh(b)="choose") then (let be =(let x1 = parbeh(beh1Choose(b),st1), x2 =parbeh(beh2Choose,st2) in union(st,(union(st1,st2))))  in 
> 				parbeh(be,st))
> 			else
> 				if (tyBeh(b)="compose") then(let be =(let x1 = parbeh(beh1Compose(b),st1), x2 =parbeh(beh2Compose,st2) in union(st,(union(st1,st2)))) in parbeh(be,st)) 
> 				 else 
> 					if (tyBeh(b)="prefix") then (let ac = trAction(b,st) in parbeh(behPrefix(b),st))
> 					else	
> 						if (tyBeh(b)="restrict") then ( let re = trRestric(consRestrict(b),st) in parbeh(behRestrict(b),st))
> 						else	done
> 						endif
> 					endif
> 				endif
> 			endif
> 		endif
> 	measure b 
> 
> but when i typechecked this, i have this error "Wrong number of arguments in measure"
> 
> thanks for answer
> 
> -------------------------------------------------------------
> NetCourrier, votre bureau virtuel sur Internet : Mail, Agenda, Clubs, Toolbar...
> Web/Wap : www.netcourrier.com
> Téléphone/Fax : 08 92 69 00 21 (0,34 € TTC/min)
> Minitel: 3615 NETCOURRIER (0,15 € TTC/min)
>