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