Parse Error

[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]
    

[hornace...@gmail.com]

Hi,

here are some things to have a look at.

1. First of all, you have a trailing comma after the Order constant
2. Second, I hope you spec is properly structured and contains the sequence of "=" to properly mark the ending of the module
3. 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

[Clifford Heath]

Also, Integers or Intergers?

Clifford Heath

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fddd802e-b36f-4778-9a53-89299496c51bn%40googlegroups.com.

[Hillel Wayne]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAPnXPY06dsxjgigtOsOcdcZQnZXYdH56kCnxXxqpiueR9gLzzQ%40mail.gmail.com.

[Khoa Goodwill]

this is what I got 

now ***Parse Error***
Encountered "/\" at line 20, column 1 in module BPlusTree and token "[]"

Residual stack trace follows:
ExtendableExpr starting at line 19, column 4.
Expression starting at line 19, column 4.
Junction Item starting at line 19, column 1.
AND-OR Junction starting at line 18, column 1.
ExtendableExpr starting at line 18, column 1.

[Khoa Goodwill]

@ hornace...@gmail.com

Thanks for the assistance. 

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

1. 1. I removed that and corrected some spelling mistakes. 
   2. it still gave parse error. 
   3. I changed it to 
   4. 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]
      
   5. 
      

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

1. 1. Yes I have the Next and Spec at the end with "===" following. 
   2. 
      

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

1. 1. 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...@gmail.com wrote:

[hornace...@gmail.com]

I see.

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