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

Re: [tlaplus] Unknown error in my model



Oh, yeah okay. Thanks!

I don't completely understand why it breaks with an error and no more information, what is happening there? Shouldn't it just complain about the temporal formula being violated?

On Tue, Dec 20, 2022 at 10:33 PM Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:
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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/Xif6yl46Kqo/unsubscribe.
To unsubscribe from this group and all its topics, 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.

--
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/CAK-z%2B%3DJ7s7Gbj4MMPajntsK6%3D44aWBFSvfObgmM%2B%3Dpygz8QGeg%40mail.gmail.com.