File: diff-trace-arrays.m

package info (click to toggle)
rumur 2020.12.20-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye
  • size: 3,292 kB
  • sloc: cpp: 17,090; ansic: 2,537; objc: 1,542; python: 1,120; sh: 538; yacc: 536; lex: 229; lisp: 15; makefile: 5
file content (29 lines) | stat: -rw-r--r-- 904 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
-- rumur_flags: ['--deadlock-detection', 'off', '--threads', '1']
-- checker_exit_code: 1
-- checker_output: None if self.xml else re.compile(r'(?!(.|\n)*\b(s\[D\]:\s*3)\b(.|\n)*\b\2\b)')

/* This model tests for regression of a bug first observed on commit
 * 7e5654ddb9ad4f3342d3c1b1abef9a3402df5dee. Certain models using enums to index
 * arrays which produced a failing counter-example, would result in a diff trace
 * that repeatedly listed an unchanging value for some members of the array. If
 * the bug has been re-introduced, this model will print the assignment 'S[D]:3'
 * multiple times in the trace.
 */

type
  t: enum { A, B, C, D, E };
  d: 0 .. 4;

var
  s: array[t] of d;

startstate begin
end;

ruleset i: t; v: d do
  rule isundefined(s[i]) & forall j: t do j = i | isundefined(s[j]) | s[j] < v end ==> begin
    s[i] := v;
  end;
end;

invariant exists i: t do isundefined(s[i]) end