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

*To*: <pvs-help@csl.sri.com>*Subject*: problem with finite types*From*: Borzoo Bonakdarpour <borzoo@cse.msu.edu>*Date*: Mon, 10 Mar 2003 19:53:04 -0500 (EST)*Sender*: pvs-help-owner@csl.sri.com

Hi, I am writing a specification to calculate the finite set of states, which have a path to a particular state. The spec looks like: reachable[state : TYPE]: THEORY BEGIN ASSUMING IMPORTING state[state] SP_is_finite : ASSUMPTION is_finite_type[StatePred] AC_is_finite : ASSUMPTION is_finite_type[Action] ENDASSUMING s0, s1 : VAR state reverse_reachable_states(x : StatePred, f : Action) : StatePred = (LAMBDA s0 : member(s0, x) AND (EXISTS (s1 : state) : member((s0, s1), f) AND member(s1, x))) fpcal (ms: StatePred, f: Action) : RECURSIVE StatePred = IF nonempty?(reverse_reachable_states(ms, f)) THEN fpcal (union(reverse_reachable_states(ms, f), ms), f) ELSE ms ENDIF MEASURE card(ms) END reachable where StatePred : TYPE = PRED[state] and Action : TYPE = PRED[[state, state]] I got a TCC: % Subtype TCC generated (at line 26, column 15) for ms % expected type S: finite_set[state] % unfinished fpcal_TCC1: OBLIGATION FORALL (ms: StatePred[state]): is_finite[state](ms); and I have reached this point in proof: {-1} is_finite_type[StatePred] |------- [1] is_finite[state](ms!1) which looks very simple, but seems there is no way to prove it. There must be something wrong somewhere else. Does anybody have any idea? Thanks, Borzoo ------------------------------------------------------------------------ Borzoo Bonakdarpour Graduate Research Assistant Department of Computer Science & Engineering Michigan State University E-mail: borzoo@cse.msu.edu URL: http://www.cse.msu.edu/~borzoo

- Prev by Date:
**Induction derivation tree** - Next by Date:
**Re: problem with finite types** - Prev by thread:
**Re: rewrite rule for expressions inside LAMBDA** - Next by thread:
**Re: problem with finite types** - Index(es):