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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sun, 1 Jun 2014 08:30:43 -0700 (PDT)*References*: <CACkJihO4vd5BjFGyfX_0DFV4DB3XLwzS2qV_v3+bDM0YJRoNFA@mail.gmail.com>

Hi Lorin,

If you read the section in Specifying Systems that describes how the

TLC model checker works, you will see that to compute the set of

states satisfying your initial predicate Init, it computes all states

satisfying TypeOK and throws away states that don't satisfy the

additional conjuncts. There are 5^25 (about 3*10^17) states

satisfying TypeOK. If you let Init equal TypeOK, TLC quickly runs out

of memory. If let Init equal TypeOK /\ FunctionsAreOnto, TLC runs

forever. These two data points should allow you to figure out what's

going on.

Cheers,

Leslie

**References**:**Using TLA+ to solve a logic puzzle***From:*Lorin Hochstein

- Prev by Date:
**Using TLA+ to solve a logic puzzle** - Next by Date:
**Re: Using TLA+ to solve a logic puzzle** - Previous by thread:
**Using TLA+ to solve a logic puzzle** - Next by thread:
**Re: Using TLA+ to solve a logic puzzle** - Index(es):