[tlaplus] Re: on tlaps

[Alex Tim <alex.timimin@xxxxxxxxx>]

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

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

Hello

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"...

Thanks.

-- 
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.