Commit 4dc23f25 authored by Hai Dang's avatar Hai Dang
Browse files

Fix queue specs instances

parent f39db1ae
......@@ -156,13 +156,14 @@ theories/examples/queue/event.v
theories/examples/queue/spec_graph.v
theories/examples/queue/spec_abs.v
theories/examples/queue/spec_abs_graph.v
theories/examples/queue/proof_ms_gps.v
theories/examples/queue/proof_ms_abs_graph.v
theories/examples/queue/proof_abs_graph_abs.v
theories/examples/queue/proof_abs_graph_graph.v
theories/examples/queue/proof_hw_graph.v
theories/examples/queue/proof_per_elem_graph.v
theories/examples/queue/proof_mp_graph.v
theories/examples/queue/proof_ms_abs_graph.v
theories/examples/queue/proof_ms_closed.v
theories/examples/queue/proof_ms_gps.v
## Chase-Lev Double-ended Queue
theories/examples/chase_lev/code.v
## Exchanger
......
......@@ -7,32 +7,33 @@ Local Open Scope Z_scope.
Section abs_graph.
Context `{!noprolG Σ, !inG Σ (graphR qevent)}.
Context (sq : spec_abs_graph.strong_queue_spec Σ).
(* We only need an extended spec with Weak Consistency *)
Context (weq : spec_abs_graph.extended_queue_spec Σ WeakQueueConsistent).
Local Existing Instances
spec_abs_graph.QueueInv_Timeless spec_abs_graph.QueueInv_Objective
spec_abs_graph.QueueLocal_Persistent.
Definition isQueue N γq q : vProp Σ := sq.(QueueLocal) N γq q .
Definition isQueue N γq q : vProp Σ := weq.(QueueLocal) N γq q .
Definition Queue γq q Q : vProp Σ := G, sq.(QueueInv) γq q Q G.
Definition Queue γq q Q : vProp Σ := G, weq.(QueueInv) γq q Q G.
#[global] Instance Queue_objective γq q Q : Objective (Queue γq q Q) := _.
#[global] Instance Queue_timeless γq q Q : Timeless (Queue γq q Q) := _.
#[global] Instance isQueue_persistent N γq q : Persistent (isQueue N γq q) := _.
Lemma new_queue_spec :
new_queue_spec' sq.(spec_abs_graph.new_queue) isQueue Queue.
new_queue_spec' weq.(spec_abs_graph.new_queue) isQueue Queue.
Proof.
iIntros (N tid Φ) "_ Post".
iApply (sq.(spec_abs_graph.new_queue_spec) with "[%//]").
iApply (weq.(spec_abs_graph.new_queue_spec) with "[%//]").
iIntros "!> * [#QL LI]". iApply "Post". iFrame "QL". by iExists _.
Qed.
Lemma enqueue_spec :
enqueue_spec' sq.(spec_abs_graph.enqueue) isQueue Queue.
enqueue_spec' weq.(spec_abs_graph.enqueue) isQueue Queue.
Proof.
intros N DISJ q tid γq V v Posx. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.enqueue_spec) with "⊒V QL"); [done..|].
awp_apply (weq.(spec_abs_graph.enqueue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "QI".
......@@ -53,10 +54,10 @@ Proof.
Qed.
Lemma dequeue_spec :
dequeue_spec' sq.(spec_abs_graph.dequeue) isQueue Queue.
dequeue_spec' weq.(spec_abs_graph.dequeue) isQueue Queue.
Proof.
intros N DISJ q tid γq V. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.dequeue_spec) with "⊒V QL"); [done..|].
awp_apply (weq.(spec_abs_graph.dequeue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "QI".
......@@ -83,10 +84,10 @@ Proof.
Qed.
Lemma try_enq_spec :
try_enq_spec' sq.(spec_abs_graph.try_enq _ _) isQueue Queue.
try_enq_spec' weq.(spec_abs_graph.try_enq) isQueue Queue.
Proof.
intros N DISJ q tid γq V v Posx. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.try_enq_spec _ _) with "⊒V QL"); [done..|].
awp_apply (weq.(spec_abs_graph.try_enq_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "QI".
......@@ -111,11 +112,11 @@ Proof.
Qed.
Lemma try_deq_spec :
try_deq_spec' sq.(spec_abs_graph.try_deq _ _) isQueue Queue.
try_deq_spec' weq.(spec_abs_graph.try_deq) isQueue Queue.
Proof.
intros N DISJ q tid γq V.
iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.try_deq_spec _ _) with "⊒V QL"); [done..|].
awp_apply (weq.(spec_abs_graph.try_deq_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "QI".
......@@ -142,22 +143,21 @@ Proof.
eapply prefix_lookup; [done|by eexists]. }
iPureIntro. by right; right.
Qed.
End abs_graph.
Program Definition abs_graph_abs_queue_spec
{Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(sq : spec_abs_graph.strong_queue_spec Σ) : queue_spec Σ := {|
spec_abs.Queue := Queue sq ;
spec_abs.isQueue := isQueue sq ;
Definition abs_graph_abs_queue_spec
Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(weq : spec_abs_graph.extended_queue_spec Σ WeakQueueConsistent) : queue_spec Σ := {|
spec_abs.Queue := Queue weq ;
spec_abs.isQueue := isQueue weq ;
spec_abs.Queue_Objective := Queue_objective sq ;
spec_abs.Queue_Timeless := Queue_timeless sq ;
spec_abs.isQueue_Persistent := isQueue_persistent sq ;
spec_abs.Queue_Objective := Queue_objective weq ;
spec_abs.Queue_Timeless := Queue_timeless weq ;
spec_abs.isQueue_Persistent := isQueue_persistent weq ;
spec_abs.new_queue_spec := new_queue_spec sq ;
spec_abs.enqueue_spec := enqueue_spec sq ;
spec_abs.dequeue_spec := dequeue_spec sq ;
spec_abs.try_enq_spec := try_enq_spec sq ;
spec_abs.try_deq_spec := try_deq_spec sq ;
spec_abs.new_queue_spec := new_queue_spec weq ;
spec_abs.enqueue_spec := enqueue_spec weq ;
spec_abs.dequeue_spec := dequeue_spec weq ;
spec_abs.try_enq_spec := try_enq_spec weq ;
spec_abs.try_deq_spec := try_deq_spec weq ;
|}%I.
......@@ -7,7 +7,7 @@ Local Open Scope Z_scope.
Section abs_graph.
Context `{!noprolG Σ, !inG Σ (graphR qevent)}.
Context (sq : spec_abs_graph.strong_queue_spec Σ).
Context `(sq : spec_abs_graph.extended_queue_spec Σ QueueConsistent).
Local Existing Instances
spec_abs_graph.QueueInv_Timeless spec_abs_graph.QueueInv_Objective
spec_abs_graph.QueueLocal_Persistent.
......@@ -21,7 +21,7 @@ Definition QueueLocal N γg q G M : vProp Σ := sq.(spec_abs_graph.QueueLocal) N
#[global] Instance QueueLocal_persistent N γg q G M : Persistent (QueueLocal N γg q G M) := _.
Lemma QueueInv_StrongQueueConsistent_instance :
γg q G, QueueInv γg q G StrongQueueConsistent G .
γg q G, QueueInv γg q G QueueConsistent G .
Proof.
intros. iDestruct 1 as (?) "QI".
by iApply sq.(spec_abs_graph.QueueInv_QueueConsistent).
......@@ -80,10 +80,10 @@ Proof.
Qed.
Lemma try_enq_spec :
try_enq_spec' sq.(spec_abs_graph.try_enq _ _) QueueLocal QueueInv.
try_enq_spec' sq.(spec_abs_graph.try_enq) QueueLocal QueueInv.
Proof.
intros N DISJ q tid γg G1 M V v Posx. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.try_enq_spec _ _) with "⊒V QL"); [done..|].
awp_apply (sq.(spec_abs_graph.try_enq_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (G) ">QI". iDestruct "QI" as (?) "QI".
iAaccIntro with "QI".
......@@ -96,10 +96,10 @@ Proof.
Qed.
Lemma try_deq_spec :
try_deq_spec' sq.(spec_abs_graph.try_deq _ _) QueueLocal QueueInv.
try_deq_spec' sq.(spec_abs_graph.try_deq) QueueLocal QueueInv.
Proof.
intros N DISJ q tid γg G1 M V. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.try_deq_spec _ _) with "⊒V QL"); [done..|].
awp_apply (sq.(spec_abs_graph.try_deq_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (G) ">QI". iDestruct "QI" as (?) "QI".
iAaccIntro with "QI".
......@@ -111,20 +111,22 @@ Proof.
Qed.
End abs_graph.
Program Definition abs_graph_abs_queue_spec
{Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(sq : spec_abs_graph.strong_queue_spec Σ) : spec_graph.strong_queue_spec Σ := {|
Definition abs_graph_graph_extended_queue_spec
Σ `{!noprolG Σ, !inG Σ (graphR qevent)} {QC}
(sq : spec_abs_graph.extended_queue_spec Σ QC)
: spec_graph.extended_queue_spec Σ QC := {|
spec_graph.extended_core_spec := {|
spec_graph.QueueInv_Objective := QueueInv_objective sq ;
spec_graph.QueueInv_Timeless := QueueInv_timeless sq ;
spec_graph.QueueLocal_Persistent := QueueLocal_persistent sq ;
spec_graph.QueueInv_QueueConsistent := QueueInv_StrongQueueConsistent_instance sq;
spec_graph.QueueInv_graph_master_acc := QueueInv_graph_master_acc_instance sq ;
spec_graph.QueueLocal_graph_snap := QueueLocal_graph_snap_instance sq ;
spec_graph.new_queue_spec := new_queue_spec sq ;
spec_graph.enqueue_spec := enqueue_spec sq ;
spec_graph.dequeue_spec := dequeue_spec sq ;
spec_graph.QueueInv_Objective := QueueInv_objective sq ;
spec_graph.QueueInv_Timeless := QueueInv_timeless sq ;
spec_graph.QueueLocal_Persistent := QueueLocal_persistent sq ;
spec_graph.QueueInv_QueueConsistent := QueueInv_StrongQueueConsistent_instance sq;
spec_graph.QueueInv_graph_master_acc := QueueInv_graph_master_acc_instance sq ;
spec_graph.QueueLocal_graph_snap := QueueLocal_graph_snap_instance sq ;
spec_graph.new_queue_spec := new_queue_spec sq ;
spec_graph.enqueue_spec := enqueue_spec sq ;
spec_graph.dequeue_spec := dequeue_spec sq ;
|} ;
spec_graph.try_enq_spec := try_enq_spec sq ;
spec_graph.try_deq_spec := try_deq_spec sq ;
spec_graph.try_enq_spec := try_enq_spec sq ;
spec_graph.try_deq_spec := try_deq_spec sq ;
|}%I.
......@@ -3578,24 +3578,3 @@ Proof.
Qed.
End proof.
Definition msqueue_impl_strong
Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
strong_queue_spec Σ := {|
spec_abs_graph.extended_core_spec := {|
spec_abs_graph.QueueInv_Objective := QueueInv_objective;
spec_abs_graph.QueueInv_QueueConsistent := QueueInv_StrongQueueConsistent_instance;
spec_abs_graph.QueueInv_graph_master_acc := QueueInv_graph_master_acc_instance;
spec_abs_graph.QueueLocal_graph_snap := QueueLocal_graph_snap_instance;
spec_abs_graph.QueueLocal_Persistent := QueueLocal_persistent;
spec_abs_graph.new_queue_spec := new_queue_spec;
spec_abs_graph.enqueue_spec := enqueue_spec;
spec_abs_graph.dequeue_spec := dequeue_spec;
|} ;
spec_abs_graph.try_enq_spec := try_enq_spec;
spec_abs_graph.try_deq_spec := try_deq_spec;
|}.
Definition msqueue_impl_weak Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
weak_queue_spec Σ :=
strong_weak_queue_spec (msqueue_impl_strong _).
From gpfsl.base_logic Require Import history. (* << for noprolG *)
From gpfsl.logic Require Import atomics.
From gpfsl.examples.queue Require Import
proof_abs_graph_abs proof_abs_graph_graph proof_ms_abs_graph.
Definition msqueue_impl_abs_graph_strong
Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_abs_graph.strong_queue_spec Σ := {|
spec_abs_graph.extended_core_spec := {|
spec_abs_graph.QueueInv_Objective := QueueInv_objective;
spec_abs_graph.QueueInv_QueueConsistent := QueueInv_StrongQueueConsistent_instance;
spec_abs_graph.QueueInv_graph_master_acc := QueueInv_graph_master_acc_instance;
spec_abs_graph.QueueLocal_graph_snap := QueueLocal_graph_snap_instance;
spec_abs_graph.QueueLocal_Persistent := QueueLocal_persistent;
spec_abs_graph.new_queue_spec := new_queue_spec;
spec_abs_graph.enqueue_spec := enqueue_spec;
spec_abs_graph.dequeue_spec := dequeue_spec;
|} ;
spec_abs_graph.try_enq_spec := try_enq_spec;
spec_abs_graph.try_deq_spec := try_deq_spec;
|}.
Definition msqueue_impl_abs_graph_weak Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_abs_graph.weak_queue_spec Σ :=
spec_abs_graph.strong_weak_queue_spec Σ (msqueue_impl_abs_graph_strong _).
Definition msqueue_impl_graph_strong Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_graph.strong_queue_spec Σ :=
proof_abs_graph_graph.abs_graph_graph_extended_queue_spec Σ
(msqueue_impl_abs_graph_strong Σ).
Definition msqueue_impl_graph_weak Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_graph.weak_queue_spec Σ :=
proof_abs_graph_graph.abs_graph_graph_extended_queue_spec Σ
(extended_strong_weak_queue_spec Σ (msqueue_impl_abs_graph_strong Σ)).
Definition msqueue_impl_abs Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_abs.queue_spec Σ :=
proof_abs_graph_abs.abs_graph_abs_queue_spec Σ
(extended_strong_weak_queue_spec Σ (msqueue_impl_abs_graph_strong Σ)).
......@@ -247,13 +247,14 @@ Qed.
End RSL.
From gpfsl.logic Require Import atomic_cmra.
From gpfsl.examples.queue Require Import code_ms proof_ms_graph.
From gpfsl.examples.queue Require Import code_ms proof_ms_abs_graph proof_ms_closed.
(* This proof can also be derived from spec_abs. *)
(* TODO: use ther spec_per_elem one. Need try_enq and try_deq *)
Section RSL_instance.
Context {Σ : gFunctors} `{noprolG Σ, !msqueueG Σ, !atomicG Σ}.
Let is_queue := QueuePerElem (msqueue_impl_weak Σ).
Let is_queue := QueuePerElem (msqueue_impl_graph_weak Σ).
Lemma per_elem_enqueue_inst N P γg q (x: Z) tid
(NZ: (0 < x)%Z) (DISJ: N ## histN) :
......
......@@ -9,6 +9,7 @@ Local Open Scope Z_scope.
Implicit Type (Q : queue) (N : namespace).
(** * Abstract State Specs, similar to Cosmo style. *)
(** Queue predicates *)
Definition isQueueT Σ : Type := namespace gname loc vProp Σ.
Definition QueueT Σ : Type := gname loc queue vProp Σ.
......
......@@ -11,6 +11,7 @@ Local Open Scope Z_scope.
Local Notation graph := (graph qevent).
Implicit Type (Q : queue) (G : graph) (M : logView).
(** * Hybrid Specs with both Abstract State and Partial Orders (Event Graph) *)
(** Queue predicate with abstract state *)
Definition QueueInvT Σ : Type :=
gname loc queue graph vProp Σ.
......@@ -184,8 +185,8 @@ Record core_queue_spec {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Arguments core_queue_spec _ {_ _} _.
Record extended_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(QueueConsistent : graph Prop) := ExtendedQueueSpec {
Record extended_queue_spec {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
{QueueConsistent : graph Prop} := ExtendedQueueSpec {
extended_core_spec :> core_queue_spec Σ QueueConsistent ;
(* extra operations *)
try_enq : val;
......@@ -196,22 +197,45 @@ Record extended_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
try_deq_spec :
try_deq_spec' try_deq extended_core_spec.(QueueLocal) extended_core_spec.(QueueInv);
}.
Arguments extended_queue_spec _ {_ _} _.
(** A strong queue spec *)
(** A Strong queue spec, with 5 operations with Strong Consistency *)
Definition strong_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
:= extended_queue_spec Σ StrongQueueConsistent.
(** A Weak queue spec *)
(** A Weak queue spec, with 3 operations and Weak Consistency *)
Definition weak_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
:= core_queue_spec Σ WeakQueueConsistent.
(** Basic queue spec *)
(** Basic queue spec, with 3 operations and Basic Consistency *)
Definition basic_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
:= core_queue_spec Σ BasicQueueConsistent.
(** Strong implies Weak *)
Program Definition extended_strong_weak_queue_spec
Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(sq : strong_queue_spec Σ) : extended_queue_spec Σ WeakQueueConsistent :=
{|
extended_core_spec := {|
QueueInv_Timeless := sq.(QueueInv_Timeless);
QueueInv_Objective := sq.(QueueInv_Objective);
QueueInv_graph_master_acc := sq.(QueueInv_graph_master_acc);
QueueLocal_graph_snap := sq.(QueueLocal_graph_snap) ;
QueueLocal_Persistent := sq.(QueueLocal_Persistent) ;
new_queue_spec := sq.(new_queue_spec) ;
enqueue_spec := sq.(enqueue_spec) ;
dequeue_spec := sq.(dequeue_spec);
|} ;
try_enq_spec := sq.(try_enq_spec) ;
try_deq_spec := sq.(try_deq_spec) ;
|}.
Next Obligation.
iIntros "* QI".
by iDestruct (sq.(QueueInv_QueueConsistent) with "QI") as %SC%strq_wkq_cons.
Qed.
Program Definition strong_weak_queue_spec
{Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(sq : strong_queue_spec Σ) : weak_queue_spec Σ :=
{|
QueueInv_Timeless := sq.(QueueInv_Timeless);
......@@ -230,7 +254,7 @@ Qed.
(** Weak implies Basic *)
Program Definition weak_basic_queue_spec
{Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(wq : weak_queue_spec Σ) : basic_queue_spec Σ :=
{|
QueueInv_Timeless := wq.(QueueInv_Timeless);
......
......@@ -11,6 +11,8 @@ Local Open Scope Z_scope.
Local Notation graph := (graph qevent).
Implicit Type (G : graph) (M : logView).
(** * Specs using Event Graphs *)
Definition unmatched_enq G eid : Prop :=
( v : Z, ge_event <$> (G.(Es) !! eid) = Some (Enq v))
( id, (eid, id) G.(so)).
......@@ -183,8 +185,8 @@ Record core_queue_spec {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Arguments core_queue_spec _ {_ _} _.
Record extended_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(QueueConsistent : graph Prop) := ExtendedQueueSpec {
Record extended_queue_spec {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
{QueueConsistent : graph Prop} := ExtendedQueueSpec {
extended_core_spec :> core_queue_spec Σ QueueConsistent ;
(* extra operations *)
try_enq : val;
......@@ -195,12 +197,13 @@ Record extended_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
try_deq_spec :
try_deq_spec' try_deq extended_core_spec.(QueueLocal) extended_core_spec.(QueueInv);
}.
Arguments extended_queue_spec _ {_ _} _.
(* only enqueue positive values *)
Definition queue_positive_value G : Prop :=
e eV (v: Z), G.(Es) !! e = Some eV eV.(ge_event) = Enq v 0 < v.
(** (2) com relates matching enqueue and dequeu events *)
(** (2) com relates matching enqueue and dequeue events *)
Definition queue_matches_value G : Prop :=
e d, (e, d) G.(com) (e < d)%nat
eV dV (v : Z), G.(Es) !! e = Some eV G.(Es) !! d = Some dV
......@@ -325,21 +328,21 @@ Record StrongQueueConsistent G : Prop := mkStrongQueueConsistent {
queue_FIFO_strong G ;
}.
(** A strong queue spec *)
(** A Strong queue spec, with 5 operations with Strong Consistency *)
Definition strong_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
:= extended_queue_spec Σ StrongQueueConsistent.
(** A Weak queue spec *)
(** A Weak queue spec, with 3 operations and Weak Consistency *)
Definition weak_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
:= core_queue_spec Σ WeakQueueConsistent.
(** Basic queue spec *)
(** Basic queue spec, with 3 operations and Basic Consistency *)
Definition basic_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
:= core_queue_spec Σ BasicQueueConsistent.
(** Strong implies Weak *)
Program Definition strong_weak_queue_spec
{Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(sq : strong_queue_spec Σ) : weak_queue_spec Σ :=
{|
QueueInv_Timeless := sq.(QueueInv_Timeless);
......@@ -358,7 +361,7 @@ Qed.
(** Weak implies Basic *)
Program Definition weak_basic_queue_spec
{Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(wq : weak_queue_spec Σ) : basic_queue_spec Σ :=
{|
QueueInv_Timeless := wq.(QueueInv_Timeless);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment