tests/while_inc.scop

   1 start: 31
   2 end: 109
   3 indent: "\t"
   4 context: '{  :  }'
   5 schedule: '{ domain: "{ S_3[t] : t >= 0; S_0[]; S_2[t] : t >= 0; S_4[]; S_1[t] : t
   6   >= 0 }", child: { sequence: [ { filter: "{ S_0[] }" }, { filter: "{ S_3[t]; S_2[t];
   7   S_1[t] }", child: { schedule: "L_0[{ S_2[t] -> [(t)]; S_3[t] -> [(t)]; S_1[t] ->
   8   [(t)] }]", child: { sequence: [ { filter: "{ S_1[t] }" }, { filter: "{ S_2[t] }"
   9   }, { filter: "{ S_3[t] }" } ] } } }, { filter: "{ S_4[] }" } ] } }'
  10 arrays:
  11 - context: '{  :  }'
  12   extent: '{ __pet_test_0[t] : t >= 0 }'
  13   value_bounds: '{ [i0] : 0 <= i0 <= 1 }'
  14   element_type: int
  15   element_size: 4
  16   uniquely_defined: 1
  17 - context: '{  :  }'
  18   extent: '{ T[i0] : i0 >= 0 }'
  19   element_type: int
  20   element_size: 4
  21 - context: '{  :  }'
  22   extent: '{ i[] }'
  23   element_type: int
  24   element_size: 4
  25 statements:
  26 - line: 5
  27   domain: '{ S_0[] }'
  28   body:
  29     type: expression
  30     expr:
  31       type: op
  32       operation: =
  33       arguments:
  34       - type: access
  35         index: '{ S_0[] -> i[] }'
  36         reference: __pet_ref_0
  37         read: 0
  38         write: 1
  39       - type: int
  40         value: 0
  41 - line: 6
  42   domain: '{ [S_1[t] -> [__pet_test_0 = 1]] : t >= 0 }'
  43   body:
  44     type: expression
  45     expr:
  46       type: op
  47       operation: =
  48       arguments:
  49       - type: access
  50         index: '{ S_1[t] -> __pet_test_0[(t)] }'
  51         reference: __pet_ref_2
  52         read: 0
  53         write: 1
  54       - type: op
  55         operation: <
  56         arguments:
  57         - type: access
  58           index: '{ S_1[t] -> i[] }'
  59           reference: __pet_ref_3
  60           read: 1
  61           write: 0
  62         - type: int
  63           value: 100
  64   arguments:
  65   - type: access
  66     index: '{ S_1[t] -> __pet_test_0[((-1 + t) : t > 0)] }'
  67     reference: __pet_ref_1
  68     read: 1
  69     write: 0
  70 - line: 7
  71   domain: '{ [S_2[t] -> [__pet_test_0 = 1]] : t >= 0 }'
  72   body:
  73     type: expression
  74     expr:
  75       type: op
  76       operation: =
  77       arguments:
  78       - type: access
  79         index: '{ [S_2[t] -> [i1]] -> T[((i1) : i1 >= 0)] }'
  80         reference: __pet_ref_6
  81         read: 0
  82         write: 1
  83         arguments:
  84         - type: access
  85           index: '{ S_2[t] -> i[] }'
  86           reference: __pet_ref_5
  87           read: 1
  88           write: 0
  89       - type: access
  90         index: '{ S_2[t] -> i[] }'
  91         reference: __pet_ref_7
  92         read: 1
  93         write: 0
  94   arguments:
  95   - type: access
  96     index: '{ S_2[t] -> __pet_test_0[(t)] }'
  97     reference: __pet_ref_4
  98     read: 1
  99     write: 0
 100 - line: 8
 101   domain: '{ [S_3[t] -> [__pet_test_0 = 1]] : t >= 0 }'
 102   body:
 103     type: expression
 104     expr:
 105       type: op
 106       operation: ++
 107       arguments:
 108       - type: access
 109         index: '{ S_3[t] -> i[] }'
 110         reference: __pet_ref_9
 111         read: 1
 112         write: 1
 113   arguments:
 114   - type: access
 115     index: '{ S_3[t] -> __pet_test_0[(t)] }'
 116     reference: __pet_ref_8
 117     read: 1
 118     write: 0
 119 - line: -1
 120   domain: '{ S_4[] }'
 121   body:
 122     type: expression
 123     expr:
 124       type: op
 125       operation: kill
 126       arguments:
 127       - type: access
 128         killed: '{ S_4[] -> i[] }'
 129         index: '{ S_4[] -> i[] }'
 130         reference: __pet_ref_10
 131         kill: 1
 132 implications:
 133 - satisfied: 1
 134   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : 0 <= t'' <= t }'