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_1[t] : t >= 0 }",
   6   child: { sequence: [ { filter: "{ S_0[] }" }, { filter: "{ S_3[t]; S_2[t]; S_1[t]
   7   }", child: { schedule: "L_0[{ S_2[t] -> [(t)]; S_1[t] -> [(t)]; S_3[t] -> [(t)]
   8   }]", child: { sequence: [ { filter: "{ S_1[t] }" }, { filter: "{ S_2[t] }" }, {
   9   filter: "{ S_3[t] }" } ] } } } ] } }'
  10 arrays:
  11 - context: '{  :  }'
  12   extent: '{ __pet_test_0[t] : t >= 0 }'
  13   value_bounds: '{ [i0] : i0 >= 0 and 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   schedule: '{ S_0[] -> [0] }'
  29   body:
  30     type: expression
  31     expr:
  32       type: op
  33       operation: =
  34       arguments:
  35       - type: access
  36         index: '{ S_0[] -> i[] }'
  37         reference: __pet_ref_0
  38         read: 0
  39         write: 1
  40       - type: int
  41         value: 0
  42 - line: 6
  43   domain: '{ [S_1[t] -> [1]] : t >= 0 }'
  44   schedule: '{ S_1[t] -> [1, t, 0] }'
  45   body:
  46     type: expression
  47     expr:
  48       type: op
  49       operation: =
  50       arguments:
  51       - type: access
  52         index: '{ S_1[t] -> __pet_test_0[(t)] }'
  53         reference: __pet_ref_2
  54         read: 0
  55         write: 1
  56       - type: op
  57         operation: <
  58         arguments:
  59         - type: access
  60           index: '{ S_1[t] -> i[] }'
  61           reference: __pet_ref_3
  62           read: 1
  63           write: 0
  64         - type: int
  65           value: 100
  66   arguments:
  67   - type: access
  68     index: '{ S_1[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
  69     reference: __pet_ref_1
  70     read: 1
  71     write: 0
  72 - line: 7
  73   domain: '{ [S_2[t] -> [1]] : t >= 0 }'
  74   schedule: '{ S_2[t] -> [1, t, 1, 0] }'
  75   body:
  76     type: expression
  77     expr:
  78       type: op
  79       operation: =
  80       arguments:
  81       - type: access
  82         index: '{ [S_2[t] -> [i1]] -> T[((i1) : i1 >= 0)] }'
  83         reference: __pet_ref_6
  84         read: 0
  85         write: 1
  86         arguments:
  87         - type: access
  88           index: '{ S_2[t] -> i[] }'
  89           reference: __pet_ref_5
  90           read: 1
  91           write: 0
  92       - type: access
  93         index: '{ S_2[t] -> i[] }'
  94         reference: __pet_ref_7
  95         read: 1
  96         write: 0
  97   arguments:
  98   - type: access
  99     index: '{ S_2[t] -> __pet_test_0[(t)] }'
 100     reference: __pet_ref_4
 101     read: 1
 102     write: 0
 103 - line: 8
 104   domain: '{ [S_3[t] -> [1]] : t >= 0 }'
 105   schedule: '{ S_3[t] -> [1, t, 1, 1] }'
 106   body:
 107     type: expression
 108     expr:
 109       type: op
 110       operation: ++
 111       arguments:
 112       - type: access
 113         index: '{ S_3[t] -> i[] }'
 114         reference: __pet_ref_9
 115         read: 1
 116         write: 1
 117   arguments:
 118   - type: access
 119     index: '{ S_3[t] -> __pet_test_0[(t)] }'
 120     reference: __pet_ref_8
 121     read: 1
 122     write: 0
 123 implications:
 124 - satisfied: 1
 125   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'