on tlaps

Alex Tim

unread,

Apr 27, 2020, 8:48:59 AM4/27/20

to tlaplus

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.

Stephan Merz

unread,

Apr 27, 2020, 8:51:51 AM4/27/20

to tla...@googlegroups.com

Does your module extend or instantiate TLAPS?

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d018bc38-2ff0-478d-99bb-1edf08eec574%40googlegroups.com.

Alex Tim

unread,

Apr 27, 2020, 9:01:06 AM4/27/20

to tlaplus

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

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

Reply all

Reply to author

Forward