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

[tlaplus] Re: on tlaps

Thanks, Stephan. Sorry im newbie. The next question is now solved also

понедельник, 27 апреля 2020 г., 15:48:59 UTC+3 пользователь Alex Tim написал:

on https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html
it is said

"In order to invoke CVC4, use the CVC4 or CVC4T identifiers in a USE or BY clause (but remember that CVC4 is not distributed with TLAPS)."

but when i try to apply a solver explicitly (even a standard one):
PROOF BY SMT (or BY Z3) it generates an exception "unknown operator"...


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6d1d7375-4b7f-4fd0-8fb4-6f9f2d38e36b%40googlegroups.com.