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

problem with finite types


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



  IMPORTING state[state]

  SP_is_finite : ASSUMPTION is_finite_type[StatePred]
  AC_is_finite : ASSUMPTION is_finite_type[Action]


  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

  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]):

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?


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