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

*From*: Carl Thuringer <carl.thuringer@xxxxxxxxx>*Date*: Mon, 6 Apr 2020 11:37:13 -0500*References*: <2523b313-25da-417d-90b8-6dbac319798d@googlegroups.com>

It seems to me that the pcal translator runs in a separate context entirely from the rest of the specification.

The `variables` statement inside of the algorithm will introduce a VARIABLES declaration in the translation.

I find it extremely helpful to study example pluscal algorithms by opening the smallest possible algorithm first, then gradually adding things as they become necessary. This has helped me learn what parts of the translation are produced by what parts of the pluscal, and where I can step outside of the algorithm, and where I must stay inside, when it comes to operators and variables.

(*-- algorithm base

begin skip;

end algorithm; *)

On Mon, Apr 6, 2020 at 11:24 AM James C <coulter.bits@xxxxxxxxx> wrote:

--I have a "tester" module that imports another "spec" module. The imported "core" module has variables that I need to substitute. Then I also need to use these variables in a PlusCal algorithm in the "tester" spec, but I cannot figure out how do so. I've searched documentation, but found nothing relevant.

---- Module Tester ----

EXTENDS Whatever

CONSTANTS Things

VARIABLES A, B

INSTANCE Core WITH VarA <- A, VarB <- B

(*--algorithm maketest

\* Reference to A or B in here result in a PCal Translator Error:

\* "Assignment to undeclared variable <variablename>"

end algorithm; *)

\* BEGIN TRANSLATION

====

Thanks,James

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/2523b313-25da-417d-90b8-6dbac319798d%40googlegroups.com.

Cheers,

Carl Thuringer

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/CAGFfb%3DY2kFcxi7ODcVCTHZZF%2BTwoAX57hqC7DV1YQVKLwZor0g%40mail.gmail.com.

**References**:**[tlaplus] Using TLA VARIABLES in PlusCal algorithm***From:*James C

- Prev by Date:
**[tlaplus] Using TLA VARIABLES in PlusCal algorithm** - Next by Date:
**[tlaplus] Re: constructing unit tests based on tlc models (tla+ specs)** - Previous by thread:
**[tlaplus] Using TLA VARIABLES in PlusCal algorithm** - Next by thread:
**Re: [tlaplus] Using TLA VARIABLES in PlusCal algorithm** - Index(es):