Re: [tlaplus] on tlaps

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Does your module extend or instantiate TLAPS?

Stephan

On 27 Apr 2020, at 14:48, Alex Tim <alex.timimin@xxxxxxxxx> wrote:

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/d018bc38-2ff0-478d-99bb-1edf08eec574%40googlegroups.com.

--
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/028232FF-7951-4AEC-B733-07159B0CAE7E%40gmail.com.