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

Re: [tlaplus] Unknown error in my model



Carefully look at this line of DataIsSomewhereCheck:

    d \in {database} \union {malformed_entities} \union {source_in}

Markus

> On Dec 20, 2022, at 12:30 PM, Marcelino Coll <marce@xxxxxxxxxxxx> wrote:
> 
> Hello! I was modeling a simple ETL framework we have to make sure we can never lose data.
> 
> When checking the model it prints:
> 
> 悪 java -XX:+UseParallelGC -jar tla2tools.jar ETL.tla -dump dot,colorize,actionlabels ETL -workers auto
> TLC2 Version 2.18 of Day Month 20?? (rev: 8a0da69)
> Running breadth-first search Model-Checking with fp 22 and seed 1979252589652203881 with 24 workers on 24 cores with 7122MB heap and 64MB offheap memory [pid: 74299] (Linux 6.0.12-arch1-1 amd64, N/A 19.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
> Parsing file /home/mcoll/capchase/code/client-monorepo/apps/metrics-api/models/ETL.tla
> Semantic processing of module ETL
> Starting... (2022-12-20 21:26:11)
> Implied-temporal checking--satisfiability problem has 1 branches.
> Computing initial states...
> Finished computing initial states: 1 distinct state generated at 2022-12-20 21:26:11.
> Error: The behavior up to this point is:
> State 1: <Initial predicate>
> /\ source_in = {1, 2, 3}
> /\ pc_source = "consume"
> /\ database = {}
> /\ pc_store = "wait"
> /\ item = FALSE
> /\ malformed_entities = {}
> /\ pc_trans = "wait"
> 
> State 2: <SourceConsume line 28, col 18 to line 34, col 77 of module ETL>
> /\ source_in = {1, 3}
> /\ pc_source = "yield"
> /\ database = {}
> /\ pc_store = "wait"
> /\ item = 2
> /\ malformed_entities = {}
> /\ pc_trans = "trans"
> 
> State 3: <Transform line 49, col 14 to line 55, col 34 of module ETL>
> /\ source_in = {1, 3}
> /\ pc_source = "anext"
> /\ database = {}
> /\ pc_store = "wait"
> /\ item = 2
> /\ malformed_entities = {2}
> /\ pc_trans = "wait"
> 
> 52 states generated, 52 distinct states found, 19 states left on queue.
> The depth of the complete state graph search is 9.
> The average outdegree of the complete state graph is 2 (minimum is 1, the maximum 3 and the 95th percentile is 2).
> Finished in 00s at (2022-12-20 21:26:11)
> Trace exploration spec path: ./ETL_TTrace_1671567971.tla
> 
> Which doesn't give any information on what the error was, only "Error: The behavior up to this point is:"
> 
> I've rechecked my model several times and I don't know what could be causing this (truthfully, I'm very new with TLA+ so it may be just me being dumb).
> 
> Attached are my model and cfg file. I also welcome any improvements over the model if you see something that is wrong or could be done better.
> 
> Thank you!
> 
> 
> ----- ETL.tla
> -------------------------------- MODULE ETL --------------------------------
> 
> CONSTANT data
> 
> VARIABLES
>     source_in,
>     database,
>     malformed_entities,
>     item,
>     pc_source,
>     pc_trans,
>     pc_store
> 
> 
> vars == << source_in, database, malformed_entities, item, pc_source, pc_trans, pc_store >>
> 
> Init == /\ source_in = data
>         /\ database = {}
>         /\ malformed_entities = {}
>         /\ pc_source = "consume"
>         /\ pc_trans = "wait"
>         /\ pc_store = "wait"
>         /\ item = FALSE
> 
> SourceConsume == \E d \in source_in:
>                     /\ pc_source = "consume"
>                     /\ item' = d
>                     /\ source_in' = source_in \ {d}
>                     /\ pc_source' = "yield"
>                     /\ pc_trans' = "trans"
>                     /\ UNCHANGED << database, malformed_entities, pc_store >>
> 
> SourceAnext == /\ pc_source = "anext"
>                /\ pc_source' = "consume"
>                /\ UNCHANGED << source_in, database, malformed_entities, item, pc_trans, pc_store >>
> 
> SourceAthrow == /\ pc_source = "athrow"
>                 /\ pc_source' = "consume"
>                 /\ source_in' = source_in \union {item}
>                 /\ UNCHANGED << database, malformed_entities, item, pc_trans, pc_store >>
> 
> Source == \/ SourceConsume
>           \/ SourceAnext
>           \/ SourceAthrow
> 
> Transform == /\ pc_trans = "trans"
>              /\ \/ /\ pc_store' = "store"
>                    /\ UNCHANGED << source_in, database, malformed_entities, item, pc_source >>
>                 \/ /\ pc_source' = "anext"
>                    /\ malformed_entities' = malformed_entities \union {item}
>                    /\ UNCHANGED << source_in, database, item, pc_store >>
>              /\ pc_trans' = "wait"
> 
> Store == /\ pc_store = "store"
>          /\ pc_source' = "anext"
>          /\ \/ /\ database' = database \union {item}
>                /\ pc_source' = "anext"
>                /\ UNCHANGED << source_in, malformed_entities, pc_trans, item >>
>             \/ /\ pc_source' = "athrow"
>                /\ UNCHANGED << source_in, database, malformed_entities, item, pc_trans >>
>          /\ pc_store' = "wait"
> 
> Fairness == /\ WF_vars(Store)
>             /\ WF_vars(Transform)
>             /\ WF_vars(Source)
> 
> Disjoint(S1, S2) == \A i \in S1: i \notin S2
>             
> DataIsSomewhereCheck == /\ \A d \in data: d \in {database} \union {malformed_entities} \union {source_in}
>            /\ Disjoint(database, malformed_entities)
>            /\ Disjoint(database, source_in)
>            /\ Disjoint(malformed_entities, source_in)
>            
> Terminating == /\ DataIsSomewhereCheck
>                /\ UNCHANGED vars           
> 
> Step == \/ Source
>         \/ Transform
>         \/ Store
> 
> Spec == Init /\ [][Step]_vars /\ Fairness
> 
> 
> DataIsSomewhere == <>[](DataIsSomewhereCheck)
> 
> =============================================================================
> 
> --- ETL.cfg
> SPECIFICATION Spec
> 
> PROPERTY DataIsSomewhere 
> 
> CONSTANT
>   data = { 1, 2, 3 }
> 
> -- 
> 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/8e875fab-6638-41b4-81ef-adc2760d5ae3n%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/1DF47FE2-31E3-4392-A8B8-FDB284749F1B%40lemmster.de.