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

Re: problem with finite types



Borzoo Bonakdarpour wrote:
> 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
> 

Hi,

The assumption is_finite_type[StatePred] specifies
that there are only finitely many functions of
type PRED[state]. That's sufficient to prove
that ms!1 is finite, but in an indirect way.

What you probably need to assume is that
there are finitely many states, that is,
"is_finite_type[state]".

Bruno
-- 
Bruno Dutertre                             | bruno@sdl.sri.com
SDL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717