Re: [tlaplus] Re: Parse Error

I suggest you take a look at the chapter 5 in Leslie's book Specifying Systems, particular at section 5.2 Functions. The chapter should help you to understand how to work with functions in TLA+.

You can find a pdf version of the book on this page https://lamport.azurewebsites.net/tla/book.html. I think that will point you in the right direction to what you are trying to accomplish.

I'd also suggest to take look at the EWD840 specification in the Examples collection of the tlaplus GitHub repository. It might be a bit advanced for you, but give a go.

Here's the link https://github.com/tlaplus/Examples/tree/master/specifications/ewd840.

Read what problem it solves first and then check the specification. Pay close attention to how the TypeOK invariant is defined there.

Hope it helps.
M.

Dátum: utorok 24. januára 2023, čas: 17:56:28 UTC+1, odosielateľ: Khoa Goodwill

@ hornace...@xxxxxxxxx
Thanks for the assistance.
First of all, you have a trailing comma after the Order constant
I removed that and corrected some spelling mistakes.
it still gave parse error.
I changed it to
VARIABLES values, versions, deleted, keys

TypeOK == /\ values \in [0..MaxKeys-1]
/\ versions \in [0..MaxKeys-1]
/\ deleted \in [0..MaxKeys-1]
/\ keys \in [0..MaxKeys-1]

Second, I hope you spec is properly structured and contains the sequence of "=" to properly mark the ending of the module
Yes I have the Next and Spec at the end with "===" following.

What are you trying to declare with the variables, is your intention to declare some arrays of given length?
I am trying to specify a storage engine with CRUD with soft delete and versioning.

I do believe i have most syntax down. but I do not understand why i keep getting errors.
On Monday, January 23, 2023 at 6:28:04 PM UTC+2 hwa...@xxxxxxxxx wrote:

Hi Khoa,

What are you learning TLA+ from? Start with a spec in that book and change it to be like what you want. Then you'll see the right syntax for things and get fewer parse errors.

H

On 1/23/2023 1:20 AM, Clifford Heath wrote:

Also, Integers or Intergers?

Clifford Heath

On Mon, 23 Jan 2023, 16:36 hornace...@xxxxxxxxx, <hornace...@xxxxxxxxx> wrote:

Hi,

here are some things to have a look at.

First of all, you have a trailing comma after the Order constant

Second, I hope you spec is properly structured and contains the sequence of "=" to properly mark the ending of the module

What are you trying to declare with the variables, is your intention to declare some arrays of given length?

M.

Dátum: nedeľa 22. januára 2023, čas: 23:45:34 UTC+1, odosielateľ: Khoa Goodwill

Hi I am getting thiis error and do not know what it is?

--------------------------- MODULE StorageEngine ---------------------------
EXTENDS TLC, Intergers, Sequences

CONSTANTS
MaxKeys, Order,

VARIABLES
values[0..MaxKeys-1],
versions[0..MaxKeys-1],
deleted[0..MaxKeys-1],
keys[0..MaxKeys-1]

--
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/fddd802e-b36f-4778-9a53-89299496c51bn%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/CAPnXPY06dsxjgigtOsOcdcZQnZXYdH56kCnxXxqpiueR9gLzzQ%40mail.gmail.com.