Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Can't come up with working model for cbc_max or spanning #114

Open
ahelwer opened this issue Jan 23, 2024 · 1 comment
Open

Can't come up with working model for cbc_max or spanning #114

ahelwer opened this issue Jan 23, 2024 · 1 comment

Comments

@ahelwer
Copy link
Collaborator

ahelwer commented Jan 23, 2024 •
edited
Loading

I'm adding basic TLC models to a bunch of specs for #107 and ran into trouble with this spec, could you help? Tagging authors @konnov @josef-widder @banhday

I'm attempting to use this model:

CONSTANTS
  N = 4
  T = 1
  F = 1
  Values = {1, 2}
  Bottom = 0
INVARIANTS TypeOK Validity Agreement
PROPERTIES Termination RealTermination
SPECIFICATION Spec
CHECK_DEADLOCK FALSE

but I get this runtime error (subtract 2 from line numbers to get the current spec, I added a couple assumptions about the constant values in my branch):

TLC2 Version 2.18 of Day Month 20?? (rev: a77ff3b)
Running breadth-first search Model-Checking with fp 16 and seed -7656258344444481100 with 8 workers on 8 cores with 3541MB heap and 64MB offheap memory [p
id: 136262] (Linux 6.6.10-arch1-1 amd64, N/A 21 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/cbc_max/cbc_max.tla
Parsing file /tmp/tlc-11021836222741093434/Integers.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-11021836222741093434/FiniteSets.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla
)
Parsing file /tmp/tlc-11021836222741093434/TLC.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-11021836222741093434/Naturals.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-11021836222741093434/Sequences.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module cbc_max
Starting... (2024-01-23 15:05:58)
Implied-temporal checking--satisfiability problem has 2 branches.
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Finished computing initial states: 81 distinct states generated at 2024-01-23 15:05:58.
Progress(5) at 2024-01-23 15:06:01: 52,442 states generated (52,442 s/min), 27,509 distinct states found (27,509 ds/min), 21,333 states left on queue.
Progress(7) at 2024-01-23 15:07:01: 2,164,207 states generated (2,111,765 s/min), 807,360 distinct states found (779,851 ds/min), 578,295 states left on q
ueue.
Progress(8) at 2024-01-23 15:08:01: 4,337,333 states generated (2,173,126 s/min), 1,525,842 distinct states found (718,482 ds/min), 1,074,077 states left 
on queue.
Progress(8) at 2024-01-23 15:09:01: 6,493,247 states generated (2,155,914 s/min), 2,219,299 distinct states found (693,457 ds/min), 1,548,647 states left 
on queue.
Progress(8) at 2024-01-23 15:10:01: 8,615,301 states generated (2,122,054 s/min), 2,904,446 distinct states found (685,147 ds/min), 2,017,726 states left 
on queue.
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to compute the value of an expression of form
CHOOSE x \in S: P, but no element of S satisfied P.
line 44, col 13 to line 45, col 75 of module cbc_max
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ sntMsgs = {}
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"BCAST1", "BCAST1", "BCAST1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {}, {}, {}>>

State 2: <BcastPhs1(1) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = {[type |-> "Phs1", value |-> 1, sndr |-> 1]}
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "BCAST1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {}, {}, {}>>

State 3: <Receive(2) line 69, col 5 to line 80, col 54 of module cbc_max>
/\ sntMsgs = {[type |-> "Phs1", value |-> 1, sndr |-> 1]}
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "BCAST1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {[type |-> "Phs1", value |-> 1, sndr |-> 1]}, {}, {}>>

State 4: <BcastPhs1(3) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = <<{}, {[type |-> "Phs1", value |-> 1, sndr |-> 1]}, {}, {}>>

State 5: <Receive(2) line 69, col 5 to line 80, col 54 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "BCAST1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
   { [type |-> "Phs1", value |-> 1, sndr |-> 1],
     [type |-> "Phs1", value |-> 3, sndr |-> 3] },
   {},
   {} >>

State 6: <BcastPhs1(4) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 2, sndr |-> 4],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "PHS1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
   { [type |-> "Phs1", value |-> 1, sndr |-> 1],
     [type |-> "Phs1", value |-> 3, sndr |-> 3] },
   {},
   {} >>

State 7: <Receive(2) line 69, col 5 to line 80, col 54 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 2, sndr |-> 4],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "BCAST1", "PHS1", "PHS1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
   { [type |-> "Phs1", value |-> 1, sndr |-> 1],
     [type |-> "Phs1", value |-> 2, sndr |-> 4],
     [type |-> "Phs1", value |-> 3, sndr |-> 3] },
   {},
   {} >>

State 8: <BcastPhs1(2) line 84, col 3 to line 87, col 52 of module cbc_max>
/\ sntMsgs = { [type |-> "Phs1", value |-> 1, sndr |-> 1],
  [type |-> "Phs1", value |-> 1, sndr |-> 2],
  [type |-> "Phs1", value |-> 2, sndr |-> 4],
  [type |-> "Phs1", value |-> 3, sndr |-> 3] }
/\ dval = <<0, 0, 0, 0>>
/\ V = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ v = <<1, 1, 3, 2>>
/\ w = <<0, 0, 0, 0>>
/\ pc = <<"PHS1", "PHS1", "PHS1", "PHS1">>
/\ nCrash = 0
/\ rcvdMsgs = << {},
   { [type |-> "Phs1", value |-> 1, sndr |-> 1],
     [type |-> "Phs1", value |-> 2, sndr |-> 4],
     [type |-> "Phs1", value |-> 3, sndr |-> 3] },
   {},
   {} >>

Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 93, column 3 to line 97, column 58 in cbc_max
1. Line 93, column 6 to line 93, column 19 in cbc_max
2. Line 94, column 6 to line 94, column 40 in cbc_max
3. Line 95, column 6 to line 95, column 65 in cbc_max
4. Line 96, column 6 to line 96, column 39 in cbc_max
5. Line 96, column 11 to line 96, column 39 in cbc_max
6. Line 96, column 29 to line 96, column 37 in cbc_max
7. Line 44, column 13 to line 45, column 75 in cbc_max


9696693 states generated, 3251762 distinct states found, 2254468 states left on queue.
The depth of the complete state graph search is 9.
Finished in 04min 34s at (2024-01-23 15:10:33)
@ahelwer ahelwer changed the title Can't come up with working model for cbc_max Can't come up with working model for cbc_max or spanning Jan 23, 2024
@ahelwer
Copy link
Collaborator Author

ahelwer commented Jan 23, 2024 •
edited
Loading

Spanning is another. A basic model fails the TypeOK check.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@ahelwer