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

Theory mucalculus with type state is not model-checkable.



Hallo,

  I am attempting to do some model-checking experiments,
and I ran into the message:

  ``Theory mucalculus with type state is not model-checkable.''

Now my type state is clearly finite, see below,
and I cannot find any hint in the prover guide telling me
what makes a type model-checkable.

What should I be looking for?


Many thanks in advance,

Wolfram Kahl


=============================================

  n : VAR nat

  maxsat  : posint = 31
  maxliq  : posint = 31
  maxwb   : posint = 15
  maxfit  : posint = 15
  maxhlth : posint = 15

  saturation(n) : bool = n <= maxsat
  liquidity(n) : bool = n <= maxliq
  wellbeing(n) : bool = n <= maxwb
  fitness(n) : bool = n <= maxfit
  health(n) : bool = n <= maxhlth

  init : [# sat:nat, liq:nat, wb:nat, fit:nat, hlth:nat #] =
         (# sat:=maxsat, liq:=maxliq, wb:=maxwb, fit:=maxfit, hlth:=maxhlth #)

  state : TYPE+ = [# sat:(saturation), liq:(liquidity), wb:(wellbeing),
                     fit:(fitness), hlth:(health)
                  #] containing init