Skip to content
Permalink
Browse files

Allow start of checking from error trace frame - #275

- Providing an RCPTT test

#275
[Feature][Toolbox]
  • Loading branch information...
quaeler committed Nov 4, 2019
1 parent 4cddc08 commit 20651e0aeaeb4b372684f579b87658c3db494f0b
@@ -0,0 +1,96 @@
--- RCPTT testcase ---
Format-Version: 1.0
Element-Name: TLA.Functional.Start.From.Error.Trace
Element-Type: testcase
Element-Version: 3.0
External-Reference: https://github.com/tlaplus/tlaplus/issues/275
Id: _r_EqIP84EemUPYAc4mFamA
Runtime-Version: 2.4.0.201902010011
Save-Time: 11/4/19, 12:23 PM
Testcase-Type: ecl

------=_.description-216f885c-d591-38ce-8ea2-e4f8cb4d6ffa
Content-Type: text/plain
Entry-Name: .description

A test for Issue 275
------=_.description-216f885c-d591-38ce-8ea2-e4f8cb4d6ffa--
------=_.content-0a7243a0-75d3-3d5f-9791-539de0e5b7ac
Content-Type: text/ecl
Entry-Name: .content

//Create Spec
OpenTLACreateNew

try -command {
with [get-editor $TLA-SPEC-NAME | get-text-viewer] {
set-text [concat "-------------------------- MODULE " $TLA-SPEC-NAME " -----------------------------\nEXTENDS Integers\nCONSTANT Proc\nCONSTANT defaultInitValue\nVARIABLES b, c, k, pc, temp\nvars == << b, c, k, pc, temp >>\nProcSet == (Proc)\nInit == /\ b = [i \in Proc |-> TRUE]\n /\ c = [i \in Proc |-> TRUE]\n /\ k \in Proc\n /\ temp = [self \in Proc |-> defaultInitValue]\n /\ pc = [self \in ProcSet |-> CASE self \in Proc -> \"Li0\"]\nLi0(self) == /\ pc[self] = \"Li0\"\n /\ b' = [b EXCEPT ![self] = FALSE]\n /\ pc' = [pc EXCEPT ![self] = \"Li1\"]\n /\ UNCHANGED << c, k, temp >>\nLi1(self) == /\ pc[self] = \"Li1\"\n /\ IF k # self\n THEN /\ pc' = [pc EXCEPT ![self] = \"Li2\"]\n ELSE /\ pc' = [pc EXCEPT ![self] = \"Li4a\"]\n /\ UNCHANGED << b, c, k, temp >>\nLi2(self) == /\ pc[self] = \"Li2\"\n /\ c' = [c EXCEPT ![self] = TRUE]\n /\ pc' = [pc EXCEPT ![self] = \"Li3a\"]\n /\ UNCHANGED << b, k, temp >>\nLi3a(self) == /\ pc[self] = \"Li3a\"\n /\ temp' = [temp EXCEPT ![self] = k]\n /\ pc' = [pc EXCEPT ![self] = \"Li3b\"]\n /\ UNCHANGED << b, c, k >>\nLi3b(self) == /\ pc[self] = \"Li3b\"\n /\ IF b[temp[self]]\n THEN /\ pc' = [pc EXCEPT ![self] = \"Li3c\"]\n ELSE /\ pc' = [pc EXCEPT ![self] = \"Li3d\"]\n /\ UNCHANGED << b, c, k, temp >>\nLi3c(self) == /\ pc[self] = \"Li3c\"\n /\ k' = self\n /\ pc' = [pc EXCEPT ![self] = \"Li3d\"]\n /\ UNCHANGED << b, c, temp >>\nLi3d(self) == /\ pc[self] = \"Li3d\"\n /\ pc' = [pc EXCEPT ![self] = \"Li1\"]\n /\ UNCHANGED << b, c, k, temp >>\nLi4a(self) == /\ pc[self] = \"Li4a\"\n /\ c' = [c EXCEPT ![self] = FALSE]\n /\ temp' = [temp EXCEPT ![self] = Proc \ {self}]\n /\ pc' = [pc EXCEPT ![self] = \"Li4b\"]\n /\ UNCHANGED << b, k >>\nLi4b(self) == /\ pc[self] = \"Li4b\"\n /\ IF temp[self] # {}\n THEN /\ \E j \in temp[self]:\n /\ temp' = [temp EXCEPT \n ![self] = temp[self] \ {j}]\n /\ IF ~c[j]\n THEN /\ pc' = [pc EXCEPT \n ![self] = \"Li1\"]\n ELSE /\ pc' = [pc EXCEPT \n ![self] = \"Li4b\"]\n ELSE /\ pc' = [pc EXCEPT ![self] = \"cs\"]\n /\ UNCHANGED temp\n /\ UNCHANGED << b, c, k >>\ncs(self) == /\ pc[self] = \"cs\"\n /\ TRUE\n /\ pc' = [pc EXCEPT ![self] = \"Li5\"]\n /\ UNCHANGED << b, c, k, temp >>\nLi5(self) == /\ pc[self] = \"Li5\"\n /\ c' = [c EXCEPT ![self] = TRUE]\n /\ pc' = [pc EXCEPT ![self] = \"Li6\"]\n /\ UNCHANGED << b, k >>\nLi6(self) == /\ pc[self] = \"Li6\"\n /\ b' = [b EXCEPT ![self] = TRUE]\n /\ pc' = [pc EXCEPT ![self] = \"ncs\"]\n /\ UNCHANGED << c, k, temp >>\nncs(self) == /\ pc[self] = \"ncs\"\n /\ TRUE\n /\ pc' = [pc EXCEPT ![self] = \"Li0\"]\n /\ UNCHANGED << b, c, k, temp >>\nP(self) == Li0(self) \/ Li1(self) \/ Li2(self) \/ Li3a(self) \/ Li3b(self)\n \/ Li3c(self) \/ Li3d(self) \/ Li4a(self) \/ Li4b(self)\n \/ cs(self) \/ Li5(self) \/ Li6(self) \/ ncs(self)\nNext == (\E self \in Proc: P(self))\nMutualExclusion == \A i, j \in Proc : \n (i # j) => ~ /\ pc[i] = \"cs\"\n /\ pc[j] = \"cs\"\nLSpec == Init /\ [][Next]_vars \n /\ \A self \in Proc: WF_vars((pc[self] # \"ncs\") /\ P(self))\nDeadlockFreedom == \n \A i \in Proc : \n (pc[i] \\notin {\"Li5\", \"Li6\", \"ncs\"}) ~> (\E j \in Proc : pc[j] = \"cs\")\n\n===================================================================\n"]
key-type "M1+s"
}

get-menu -path $TLA-MENU-PATH-NEW-MODEL | click
get-window $TLA-DIALOG-TITLE-NEW-MODEL | get-button $TLA-BUTTON-OK | click

with [get-editor $TLA-MODEL-ONE] {
with [get-section $TLA-MO-ED-OVERVIEW-SECTION-SPEC] {
get-combo | select "Temporal formula"
get-text-viewer | set-text "LSpec"
}
with [get-section $TLA-MO-ED-OVERVIEW-SECTION-MODEL] {
get-table | select "Proc <- "
get-button $TLA-BUTTON-EDIT | click
with [get-window -class WizardDialog] {
get-text-viewer | type-text "{ p1, p2, p3 }"
get-button "Set of model values" | click
get-button $TLA-BUTTON-FINISH | click
}
}
with [get-section $TLA-MO-ED-OVERVIEW-SECTION-CHECK] {
get-button $TLA-BUTTON-DEADLOCK | check
with [get-section $TLA-MO-ED-OVERVIEW-SECTION-CHECK-INV] {
click
get-button $TLA-BUTTON-ADD | click
with [get-window -class WizardDialog] {
get-text-viewer | type-text "MutualExclusion"
get-button $TLA-BUTTON-FINISH | click
}
}
with [get-section $TLA-MO-ED-OVERVIEW-SECTION-CHECK-PROP] {
click
get-button $TLA-BUTTON-ADD | click
with [get-window -class WizardDialog] {
get-text-viewer | type-text "DeadlockFreedom"
get-button $TLA-BUTTON-FINISH | click
}
}
}
}

get-menu -path "TLC Model Checker/Run model" | click

wait-run

with [get-view $TLA-VIEW-TLC-ERRORS | get-section $TLA-MO-ED-TLCERRORS-SECTION-ET | get-tree] {
select " <Li0 line 13, col 14 to line 16, col 42 of module new>" | mouse down Right
get-menu -path "Run model from this point" | click
}

get-window "Model Reconfigured" | get-button OK | click

with [get-editor $TLA-MODEL-ONE | get-section $TLA-MO-ED-OVERVIEW-SECTION-SPEC ] {
get-combo | get-text | equals "Initial predicate and next-state" | verify-true
get-text-viewer -after [get-label "Next:"] | get-text | equals "LSpec" | verify-true
// In no possible contortion could i get the equals operator to play nice with the backslashes we were
// getting back in the get-text below; so i replaced them in the text.
global [val scrubbed ""]
get-text-viewer -after [get-label "Init:"] | get-text | split -sep "/\\\\" -trimResults | foreach [val item] {
global [val scrubbed [concat $scrubbed "CONJ" $item]] -override
}
concat $scrubbed | equals "CONJCONJb = (p1 :> FALSE @@ p2 :> TRUE @@ p3 :> TRUE)CONJc = (p1 :> TRUE @@ p2 :> TRUE @@ p3 :> TRUE)CONJk = p1CONJpc = (p1 :> \"Li1\" @@ p2 :> \"Li0\" @@ p3 :> \"Li0\")CONJtemp = (p1 :> defaultInitValue @@ p2 :> defaultInitValue @@ p3 :> defaultInitValue)" | verify-true
}

get-menu -path "File/Save" | click
} -finally {
DeleteSpecNew
}
------=_.content-0a7243a0-75d3-3d5f-9791-539de0e5b7ac--
@@ -5,7 +5,7 @@ Element-Type: testsuite
Element-Version: 2.0
Id: _XtCd4APNEemtrbArmQOOJA
Runtime-Version: 2.4.0.201902010011
Save-Time: 10/12/19, 10:10 AM
Save-Time: 11/4/19, 12:24 PM

------=_testcase-items-62c497da-4241-31f4-811a-6b453a3ecff8
Content-Type: text/testcase
@@ -49,5 +49,6 @@ _JObaIIvTEemXYtOZX2zpng // kind: 'test' name: 'TLA.Functional.ECE.Placement' pat
_RifTcLZDEemcF9BXFSE9ew // kind: 'test' name: 'TLA.Functional.TLAPS' path: 'TLA.Functional.TLAPS.test'
_wH2aMNWzEemOp9qASlV00A // kind: 'test' name: 'TLA.Functional.PCal.Checksums' path: 'TLA.Functional.PCal.Checksums.test'
_BbLbgO0TEemu8qbF8JrHog // kind: 'test' name: 'TLA.Functional.Error.Trace' path: 'TLA.Functional.Error.Trace.test'
_r_EqIP84EemUPYAc4mFamA // kind: 'test' name: 'TLA.Functional.Start.From.Error.Trace' path: 'TLA.Functional.Start.From.Error.Trace.test'

------=_testcase-items-62c497da-4241-31f4-811a-6b453a3ecff8--

0 comments on commit 20651e0

Please sign in to comment.
You can’t perform that action at this time.