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

*From*: "christin...@xxxxxxxxx" <christina.a.burge@xxxxxxxxx>*Date*: Tue, 11 Jul 2023 08:40:25 -0700 (PDT)*References*: <c76a27c0-2188-4620-8e77-f4b9de8904b5n@googlegroups.com> <4B8DB10E-3290-4AAB-926E-8F57F77A17F0@gmail.com>

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 declarationvariables [...] 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,StephanOn 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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f8a8171f-c661-480c-a37b-150a075f165an%40googlegroups.com.

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

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

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

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