← Back to branch summary

~tapaal-dist/verifypn/verifypnLTSmin

« back to all changes in this revision

Viewing changes to INPUT_MC/TokenRing-PT-005/ReachabilityComputeBounds.txt

  • Committer: Mads Johannsen
  • Date: 2015-05-27 01:37:47 UTC
  • Revision ID: mjohan12@student.aau.dk-20150527013747-fc4uexe0yfjsw7pm
Directory cleanup and readme

Show diffs side-by-side

added added

removed removed

Lines of Context:
INPUT_MC/TokenRing-PT-005/ReachabilityComputeBounds.txt
1
 
Property TokenRing-COL-005-ReachabilityComputeBounds-0
2
 
  "Automatically generated"
3
 
  is:
4
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
5
 
  end.
6
 
Property TokenRing-COL-005-ReachabilityComputeBounds-1
7
 
  "Automatically generated"
8
 
  is:
9
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
10
 
  end.
11
 
Property TokenRing-COL-005-ReachabilityComputeBounds-2
12
 
  "Automatically generated"
13
 
  is:
14
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
15
 
  end.
16
 
Property TokenRing-COL-005-ReachabilityComputeBounds-3
17
 
  "Automatically generated"
18
 
  is:
19
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
20
 
  end.
21
 
Property TokenRing-COL-005-ReachabilityComputeBounds-4
22
 
  "Automatically generated"
23
 
  is:
24
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
25
 
  end.
26
 
Property TokenRing-COL-005-ReachabilityComputeBounds-5
27
 
  "Automatically generated"
28
 
  is:
29
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
30
 
  end.
31
 
Property TokenRing-COL-005-ReachabilityComputeBounds-6
32
 
  "Automatically generated"
33
 
  is:
34
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
35
 
  end.
36
 
Property TokenRing-COL-005-ReachabilityComputeBounds-7
37
 
  "Automatically generated"
38
 
  is:
39
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
40
 
  end.
41
 
Property TokenRing-COL-005-ReachabilityComputeBounds-8
42
 
  "Automatically generated"
43
 
  is:
44
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
45
 
  end.
46
 
Property TokenRing-COL-005-ReachabilityComputeBounds-9
47
 
  "Automatically generated"
48
 
  is:
49
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
50
 
  end.
51
 
Property TokenRing-COL-005-ReachabilityComputeBounds-10
52
 
  "Automatically generated"
53
 
  is:
54
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
55
 
  end.
56
 
Property TokenRing-COL-005-ReachabilityComputeBounds-11
57
 
  "Automatically generated"
58
 
  is:
59
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
60
 
  end.
61
 
Property TokenRing-COL-005-ReachabilityComputeBounds-12
62
 
  "Automatically generated"
63
 
  is:
64
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
65
 
  end.
66
 
Property TokenRing-COL-005-ReachabilityComputeBounds-13
67
 
  "Automatically generated"
68
 
  is:
69
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
70
 
  end.
71
 
Property TokenRing-COL-005-ReachabilityComputeBounds-14
72
 
  "Automatically generated"
73
 
  is:
74
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
75
 
  end.
76
 
Property TokenRing-COL-005-ReachabilityComputeBounds-15
77
 
  "Automatically generated"
78
 
  is:
79
 
    bound("State_3_1", "State_1_3", "State_4_4", "State_5_2", "State_3_0", "State_0_4", "State_4_1", "State_1_5", "State_4_2", "State_0_5", "State_2_0", "State_1_4", "State_3_2", "State_4_3", "State_4_0", "State_5_3", "State_5_0", "State_3_5", "State_2_5", "State_2_2", "State_4_5", "State_0_1", "State_1_2", "State_3_4", "State_1_1", "State_2_3", "State_2_4", "State_0_2", "State_5_5", "State_3_3", "State_0_3", "State_5_1", "State_5_4", "State_2_1", "State_1_0", "State_0_0")
80
 
  end.