Commit b206e119 authored by Jaehwang Jung's avatar Jaehwang Jung Committed by Hai Dang
Browse files

Move queue event to a separate file

parent c0dd63f2
......@@ -152,6 +152,7 @@ theories/examples/queue/spec_per_elem.v
theories/examples/queue/code_ms.v
theories/examples/queue/code_hw.v
theories/examples/queue/code_producer_consumer.v
theories/examples/queue/event.v
theories/examples/queue/spec_graph.v
theories/examples/queue/proof_ms_gps.v
theories/examples/queue/proof_ms_graph.v
......
From stdpp Require Import countable.
Require Import iris.prelude.options.
(** Queue events *)
Inductive qevent := Enq (v : Z) | Deq (v : Z) | EmpDeq (* | FAIL_DEQ *).
Notation dummy_qevt := (Enq 0).
Local Open Scope Z_scope.
Instance qevent_eq_dec : EqDecision qevent.
Proof. solve_decision. Defined.
Instance qevent_countable : Countable qevent.
Proof.
refine (
inj_countable'
(λ e, match e with
| Enq v => (1, v)
| Deq v => (2, v)
| EmpDeq => (3, 0) end)
(λ x, match x with
| (1, v) => Enq v
| (2, v) => Deq v
| _ => EmpDeq end) _);
by intros [].
Qed.
Definition is_enqueue e v : Prop := e = Enq v.
Definition is_dequeue e v : Prop := e = Deq v.
Definition is_maybe_dequeue e : Prop :=
match e with | Enq _ => False | _ => True end.
......@@ -2,32 +2,12 @@ From stdpp Require Import namespaces.
From gpfsl.logic Require Import logatom.
From gpfsl.examples.graph Require Export spec.
From gpfsl.examples.queue Require Export event.
Require Import iris.prelude.options.
Local Open Scope Z_scope.
(** Queue events *)
Inductive qevent := Enq (v : Z) | Deq (v : Z) | EmpDeq (* | FAIL_DEQ *).
Notation dummy_qevt := (Enq 0).
Instance qevent_eq_dec : EqDecision qevent.
Proof. solve_decision. Defined.
Instance qevent_countable : Countable qevent.
Proof.
refine (
inj_countable'
(λ e, match e with
| Enq v => (1, v)
| Deq v => (2, v)
| EmpDeq => (3, 0) end)
(λ x, match x with
| (1, v) => Enq v
| (2, v) => Deq v
| _ => EmpDeq end) _);
by intros [].
Qed.
Local Notation graph := (graph qevent).
Implicit Type (G : graph) (M : logView).
......@@ -36,11 +16,6 @@ Definition unmatched_enq G eid : Prop :=
( id, (eid, id) G.(so)).
(** Queue predicates *)
Definition is_enqueue e v : Prop := e = Enq v.
Definition is_dequeue e v : Prop := e = Deq v.
Definition is_maybe_dequeue e : Prop :=
match e with | Enq _ => False | _ => True end.
Definition QueueLocalT Σ : Type :=
namespace gname loc graph logView vProp Σ.
Definition QueueInvT Σ : Type :=
......
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