← Back to branch summary

~tapaal-dist/verifypn/verifypnLTSmin

« back to all changes in this revision

Viewing changes to INPUT_MC/SharedMemory-PT-000010/ReachabilityCardinality.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/SharedMemory-PT-000010/ReachabilityCardinality.txt
1
 
Property SharedMemory-COL-000010-ReachabilityCardinality-0
2
 
  "Automatically generated"
3
 
  is:
4
 
    E F ! ((! ((3) <= (#tokens("Ext_Bus")))) & (((((2) <= (#tokens("Queue_6", "Queue_5", "Queue_4", "Queue_3", "Queue_2", "Queue_1", "Queue_10", "Queue_9", "Queue_8", "Queue_7")))) | (((#tokens("Ext_Bus")) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))))))
5
 
  end.
6
 
Property SharedMemory-COL-000010-ReachabilityCardinality-1
7
 
  "Automatically generated"
8
 
  is:
9
 
    A G ! ! ((((#tokens("Ext_Bus")) <= (#tokens("Ext_Bus")))) | (((#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))))
10
 
  end.
11
 
Property SharedMemory-COL-000010-ReachabilityCardinality-2
12
 
  "Automatically generated"
13
 
  is:
14
 
    A G ((((((((1) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))) | (((3) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))))) | (! ((3) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))))) | (((((((3) <= (#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")))) & (((2) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))))) | (((((1) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))) & (((3) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))))))))
15
 
  end.
16
 
Property SharedMemory-COL-000010-ReachabilityCardinality-3
17
 
  "Automatically generated"
18
 
  is:
19
 
    A G ((((2) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))) & (! ((((#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")) <= (#tokens("OwnMemAcc_4", "OwnMemAcc_3", "OwnMemAcc_2", "OwnMemAcc_1", "OwnMemAcc_6", "OwnMemAcc_5", "OwnMemAcc_8", "OwnMemAcc_7", "OwnMemAcc_10", "OwnMemAcc_9")))) & (((3) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))))))
20
 
  end.
21
 
Property SharedMemory-COL-000010-ReachabilityCardinality-4
22
 
  "Automatically generated"
23
 
  is:
24
 
    E F ! ((3) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))
25
 
  end.
26
 
Property SharedMemory-COL-000010-ReachabilityCardinality-5
27
 
  "Automatically generated"
28
 
  is:
29
 
    E F ((#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))
30
 
  end.
31
 
Property SharedMemory-COL-000010-ReachabilityCardinality-6
32
 
  "Automatically generated"
33
 
  is:
34
 
    E F ((((3) <= (#tokens("Ext_Bus")))) & (! ((((#tokens("Ext_Bus")) <= (#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")))) & (((1) <= (#tokens("OwnMemAcc_4", "OwnMemAcc_3", "OwnMemAcc_2", "OwnMemAcc_1", "OwnMemAcc_6", "OwnMemAcc_5", "OwnMemAcc_8", "OwnMemAcc_7", "OwnMemAcc_10", "OwnMemAcc_9")))))))
35
 
  end.
36
 
Property SharedMemory-COL-000010-ReachabilityCardinality-7
37
 
  "Automatically generated"
38
 
  is:
39
 
    E F ! ((((((#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")) <= (#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")))) & (((#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))))) | (((((2) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))) | (((#tokens("Queue_6", "Queue_5", "Queue_4", "Queue_3", "Queue_2", "Queue_1", "Queue_10", "Queue_9", "Queue_8", "Queue_7")) <= (#tokens("Ext_Bus")))))))
40
 
  end.
41
 
Property SharedMemory-COL-000010-ReachabilityCardinality-8
42
 
  "Automatically generated"
43
 
  is:
44
 
    E F ((((1) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))) & (((((((3) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))) | (((#tokens("Queue_6", "Queue_5", "Queue_4", "Queue_3", "Queue_2", "Queue_1", "Queue_10", "Queue_9", "Queue_8", "Queue_7")) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))))) & (! ((2) <= (#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")))))))
45
 
  end.
46
 
Property SharedMemory-COL-000010-ReachabilityCardinality-9
47
 
  "Automatically generated"
48
 
  is:
49
 
    A G ((((((#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")) <= (#tokens("Queue_6", "Queue_5", "Queue_4", "Queue_3", "Queue_2", "Queue_1", "Queue_10", "Queue_9", "Queue_8", "Queue_7")))) & (((((2) <= (#tokens("Queue_6", "Queue_5", "Queue_4", "Queue_3", "Queue_2", "Queue_1", "Queue_10", "Queue_9", "Queue_8", "Queue_7")))) | (((#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")) <= (#tokens("OwnMemAcc_4", "OwnMemAcc_3", "OwnMemAcc_2", "OwnMemAcc_1", "OwnMemAcc_6", "OwnMemAcc_5", "OwnMemAcc_8", "OwnMemAcc_7", "OwnMemAcc_10", "OwnMemAcc_9")))))))) | (! ((2) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))))
50
 
  end.
51
 
Property SharedMemory-COL-000010-ReachabilityCardinality-10
52
 
  "Automatically generated"
53
 
  is:
54
 
    A G ((#tokens("Queue_6", "Queue_5", "Queue_4", "Queue_3", "Queue_2", "Queue_1", "Queue_10", "Queue_9", "Queue_8", "Queue_7")) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))
55
 
  end.
56
 
Property SharedMemory-COL-000010-ReachabilityCardinality-11
57
 
  "Automatically generated"
58
 
  is:
59
 
    A G ((#tokens("Ext_Bus")) <= (#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")))
60
 
  end.
61
 
Property SharedMemory-COL-000010-ReachabilityCardinality-12
62
 
  "Automatically generated"
63
 
  is:
64
 
    E F ! ((#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))
65
 
  end.
66
 
Property SharedMemory-COL-000010-ReachabilityCardinality-13
67
 
  "Automatically generated"
68
 
  is:
69
 
    A G ((! ! ((#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")) <= (#tokens("Memory_2", "Memory_1", "Memory_9", "Memory_10", "Memory_7", "Memory_8", "Memory_5", "Memory_6", "Memory_3", "Memory_4")))) | (((#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")) <= (#tokens("Queue_6", "Queue_5", "Queue_4", "Queue_3", "Queue_2", "Queue_1", "Queue_10", "Queue_9", "Queue_8", "Queue_7")))))
70
 
  end.
71
 
Property SharedMemory-COL-000010-ReachabilityCardinality-14
72
 
  "Automatically generated"
73
 
  is:
74
 
    E F ((! ((((#tokens("OwnMemAcc_4", "OwnMemAcc_3", "OwnMemAcc_2", "OwnMemAcc_1", "OwnMemAcc_6", "OwnMemAcc_5", "OwnMemAcc_8", "OwnMemAcc_7", "OwnMemAcc_10", "OwnMemAcc_9")) <= (#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")))) & (((1) <= (#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")))))) & (! ((((1) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))) | (((3) <= (#tokens("Ext_Mem_Acc_2_1", "Ext_Mem_Acc_3_1", "Ext_Mem_Acc_4_1", "Ext_Mem_Acc_5_1", "Ext_Mem_Acc_6_1", "Ext_Mem_Acc_7_1", "Ext_Mem_Acc_8_1", "Ext_Mem_Acc_9_1", "Ext_Mem_Acc_10_1", "Ext_Mem_Acc_1_2", "Ext_Mem_Acc_3_2", "Ext_Mem_Acc_4_2", "Ext_Mem_Acc_5_2", "Ext_Mem_Acc_7_2", "Ext_Mem_Acc_6_2", "Ext_Mem_Acc_9_2", "Ext_Mem_Acc_8_2", "Ext_Mem_Acc_1_3", "Ext_Mem_Acc_10_2", "Ext_Mem_Acc_4_3", "Ext_Mem_Acc_2_3", "Ext_Mem_Acc_6_3", "Ext_Mem_Acc_5_3", "Ext_Mem_Acc_8_3", "Ext_Mem_Acc_7_3", "Ext_Mem_Acc_10_3", "Ext_Mem_Acc_9_3", "Ext_Mem_Acc_2_4", "Ext_Mem_Acc_1_4", "Ext_Mem_Acc_6_4", "Ext_Mem_Acc_7_4", "Ext_Mem_Acc_3_4", "Ext_Mem_Acc_5_4", "Ext_Mem_Acc_10_4", "Ext_Mem_Acc_1_5", "Ext_Mem_Acc_8_4", "Ext_Mem_Acc_9_4", "Ext_Mem_Acc_4_5", "Ext_Mem_Acc_6_5", "Ext_Mem_Acc_2_5", "Ext_Mem_Acc_3_5", "Ext_Mem_Acc_9_5", "Ext_Mem_Acc_10_5", "Ext_Mem_Acc_7_5", "Ext_Mem_Acc_8_5", "Ext_Mem_Acc_4_6", "Ext_Mem_Acc_3_6", "Ext_Mem_Acc_2_6", "Ext_Mem_Acc_1_6", "Ext_Mem_Acc_9_6", "Ext_Mem_Acc_8_6", "Ext_Mem_Acc_7_6", "Ext_Mem_Acc_5_6", "Ext_Mem_Acc_3_7", "Ext_Mem_Acc_2_7", "Ext_Mem_Acc_1_7", "Ext_Mem_Acc_10_6", "Ext_Mem_Acc_8_7", "Ext_Mem_Acc_6_7", "Ext_Mem_Acc_5_7", "Ext_Mem_Acc_4_7", "Ext_Mem_Acc_3_8", "Ext_Mem_Acc_4_8", "Ext_Mem_Acc_5_8", "Ext_Mem_Acc_6_8", "Ext_Mem_Acc_9_7", "Ext_Mem_Acc_10_7", "Ext_Mem_Acc_1_8", "Ext_Mem_Acc_2_8", "Ext_Mem_Acc_2_9", "Ext_Mem_Acc_3_9", "Ext_Mem_Acc_4_9", "Ext_Mem_Acc_5_9", "Ext_Mem_Acc_7_8", "Ext_Mem_Acc_9_8", "Ext_Mem_Acc_10_8", "Ext_Mem_Acc_1_9", "Ext_Mem_Acc_2_10", "Ext_Mem_Acc_1_10", "Ext_Mem_Acc_4_10", "Ext_Mem_Acc_3_10", "Ext_Mem_Acc_7_9", "Ext_Mem_Acc_6_9", "Ext_Mem_Acc_10_9", "Ext_Mem_Acc_8_9", "Ext_Mem_Acc_9_10", "Ext_Mem_Acc_6_10", "Ext_Mem_Acc_5_10", "Ext_Mem_Acc_8_10", "Ext_Mem_Acc_7_10")))))))
75
 
  end.
76
 
Property SharedMemory-COL-000010-ReachabilityCardinality-15
77
 
  "Automatically generated"
78
 
  is:
79
 
    E F ! ((((#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")) <= (#tokens("Active_7", "Active_8", "Active_5", "Active_6", "Active_3", "Active_4", "Active_1", "Active_2", "Active_10", "Active_9")))) | (((((3) <= (#tokens("Queue_6", "Queue_5", "Queue_4", "Queue_3", "Queue_2", "Queue_1", "Queue_10", "Queue_9", "Queue_8", "Queue_7")))) & (((1) <= (#tokens("OwnMemAcc_4", "OwnMemAcc_3", "OwnMemAcc_2", "OwnMemAcc_1", "OwnMemAcc_6", "OwnMemAcc_5", "OwnMemAcc_8", "OwnMemAcc_7", "OwnMemAcc_10", "OwnMemAcc_9")))))))
80
 
  end.