added ISL part

Test/civl/inductive-sequentialization/snapshot-scatter-gather.bpl

@@ -121,4 +121,79 @@ modifies channels;
     assume channels[tid] != None();
     snapshot := channels[tid]->t;
     channels[tid] := None();
-}
+}
+
+async action {:layer 1} main_s(tid: Tid, {:linear_in} sps: Set Permission)
+refines {:IS_left} main_s' using Inv_s;
+modifies pSet;
+creates read_s;
+{
+    assume {:add_to_pool "A", 0, n} true;
+    assert sps == WholeTidPermission(tid);
+    assert channels[tid] == None();
+    call create_asyncs((lambda pa:read_s :: 1 <= pa->perm->val->mem_index && pa->perm->val->mem_index <= n && pa->perm->val->tid == tid));
+}
+
+action {:layer 2} main_s'(tid: Tid, {:linear_in} sps: Set Permission)
+modifies pSet, channels;
+{
+    var snapshot: [int]StampedValue;  
+    assume {:add_to_pool "A", 0, n} true;
+    assert sps == WholeTidPermission(tid);
+    assert channels[tid] == None();
+    assume (forall i:int :: 1 <= i && i <= n ==> (snapshot[i]->ts > mem[i]->ts  || snapshot[i]== mem[i]));
+    call Set_Put(pSet, sps);
+    call ChannelSend(tid, snapshot);
+}
+
+async left action {:layer 1} read_s({:linear_in} perm: One Permission)
+modifies snapshots, pSet, channels;
+{
+    var {:pool "K"} k:int;
+    var {:pool "V"} v:Value;
+    assert 1 <= perm->val->mem_index && perm->val->mem_index <=n;
+    assume {:add_to_pool "A", 0, n} true;
+
+    if (*) {
+        assume {:add_to_pool "K", mem[perm->val->mem_index]->ts, k} {:add_to_pool "V", mem[perm->val->mem_index]->value, v} true;
+        assume k > mem[perm->val->mem_index]->ts; 
+        snapshots[perm->val->tid][perm->val->mem_index]:= StampedValue(k, v);
+    } else {
+        snapshots[perm->val->tid][perm->val->mem_index]:= mem[perm->val->mem_index];
+    }
+    call One_Put(pSet, perm);
+
+    if (Set_IsSubset(WholeTidPermission(perm->val->tid), pSet)) {
+        call ChannelSend(perm->val->tid, snapshots[perm->val->tid]);
+    }
+}
+
+action {:layer 1} Inv_s(tid: Tid, {:linear_in} sps: Set Permission)
+modifies snapshots, pSet, channels;
+creates read_s;
+{
+    var {:pool "A"} j: int;
+    var {:linear} sps': Set Permission;
+    var {:linear} done_set: Set Permission;
+    var choice: read_s;
+    assert sps == WholeTidPermission(tid);
+    assert channels[tid] == None();
+    assume {:add_to_pool "A", 0, j+1, n} 0 <= j && j <= n;
+    havoc snapshots;
+    assume (forall i:int :: 1 <= i && i <= j ==> (snapshots[tid][i]->ts > mem[i]->ts || snapshots[tid][i]== mem[i]));
+
+    assume {:add_to_pool "D", Permission(tid, n)} true;
+    sps' := sps;
+    call done_set := Set_Get(sps', (lambda {:pool "D" } x: Permission :: x->tid == tid && 1 <= x->mem_index && x->mem_index <= j));
+
+    call Set_Put(pSet, done_set);
+    if (j < n) {
+        choice := read_s(One(Permission(tid, j+1)));
+        assume {:add_to_pool "C", choice} true;
+        call create_asyncs((lambda {:pool "C" } pa:read_s :: j+1 <=  pa->perm->val->mem_index && pa->perm->val->mem_index <= n && pa->perm->val->tid == tid));
+        call set_choice(choice);
+    } else {
+        call ChannelSend(tid, snapshots[tid]);
+    }
+}
+