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

*From*: "christin...@xxxxxxxxx" <christina.a.burge@xxxxxxxxx>*Date*: Mon, 24 Jul 2023 16:07:49 -0700 (PDT)*References*: <c76a27c0-2188-4620-8e77-f4b9de8904b5n@googlegroups.com> <4B8DB10E-3290-4AAB-926E-8F57F77A17F0@gmail.com> <f8a8171f-c661-480c-a37b-150a075f165an@googlegroups.com> <1ef58e75-fd21-58fb-52ec-479d1f8f4a50@gmail.com>

Thank you! I have it working now.

On Tuesday, July 11, 2023 at 9:36:54 PM UTC+1 Hillel Wayne wrote:

The problem is that

..is imported from theIntegersmodule, which TLC doesn't know about.You instead have to do something like make a newMaxValueconstant, defineValue == 0..MaxValue, and then in the config file setMaxValue = 10.(You

canassign0..10to a constant in the Toolbox IDE, which works by defining a newMC.tlafile withConst_1234 == 0..10, and then puttingValue <- Const_1234in the config file.)

H

On 7/11/2023 10:40 AM, christin...@xxxxxxxxx wrote:

Ack, so silly not to spot that I'd set it to zero myself! Thank you!

Another entry-level question: if I want to set Value in a .cfg file, how do I do that? I've tried:

SPECIFICATION Spec

CONSTANTS

n = 10

Value = 0..10

And variations ( Value == ..., Value <- ...) but I continue to get errors.

Error: TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a tlc2.tool.ConfigFileException

: TLC found an error in the configuration file at line 4

It was expecting = or <-, but did not find it.

Finished in 00s at (2023-07-11 17:35:05)

Any advice welcome!

--On Monday, July 10, 2023 at 1:52:15 PM UTC+1 Stephan Merz wrote:

The declaration

variables [...] value, array = [k \in 1 .. n |-> 0]

initializes all array elements to zero. Also, the PlusCal translator initializes `value` to a default value (that will be different from standard values such as integers).

Instead, you could parameterize your specification by introducing a set Value as follows:

CONSTANT n, Value

[...]

variables [...], value \in Value, array \in [1..n -> Value]

In this way, `value` will be a non-deterministically chosen element of the parameter set and `array` will be non-deterministically initialized to hold values in that set.

When running TLC, you'll instantiate the parameter Value by a specific set such as 0 .. 3 (an interval of integers), {"a", "b", "c"} (a set of strings) or {v1, v2, v3} (a set of abstract "model" values).

Hope this helps,Stephan

On 10 Jul 2023, at 14:10, christin...@xxxxxxxxx <christin...@xxxxxxxxx> wrote:

I have been thinking about ways to verify C++ templates, and I wonder if TLA+ would be good for this?

I can quite trivially (for example) write a PlusCal spec to verify std::find for a specific input type, but is there a way to explore the state space for all types of data that might be in the array?

I have the below, which does not initialise the array to be anything, but that seems to default set it to zero.

-------------------------------- MODULE find -------------------

EXTENDS Naturals, TLC, Integers

CONSTANT n

(* --algorithm find

variables first = 1, last \in 1 .. n , value, array = [k \in 1 .. n |-> 0],

begin

assert last >= first;

while first /= last do

if array[first] = value then

skip;

end if;

first := first + 1;

end while;

end algorithm *)

--

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c76a27c0-2188-4620-8e77-f4b9de8904b5n%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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f8a8171f-c661-480c-a37b-150a075f165an%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/aa5df4a6-ca3d-4cfc-be5e-79dfc0850aa7n%40googlegroups.com.

**References**:**[tlaplus] TLA+ and C++ templates***From:*christin...@xxxxxxxxx

**Re: [tlaplus] TLA+ and C++ templates***From:*Stephan Merz

**Re: [tlaplus] TLA+ and C++ templates***From:*christin...@xxxxxxxxx

**Re: [tlaplus] TLA+ and C++ templates***From:*Hillel Wayne

- Prev by Date:
**Re: [tlaplus] Directed Graph from Specifying Systems** - Next by Date:
**Re: [tlaplus] Directed Graph from Specifying Systems** - Previous by thread:
**Re: [tlaplus] TLA+ and C++ templates** - Next by thread:
**[tlaplus] About stuttering steps, deadlock and Implementation** - Index(es):