Commit cbc347da authored by Hai Dang's avatar Hai Dang
Browse files

Move stack event to a separate file

parent 86b94266
......@@ -128,6 +128,7 @@ theories/examples/circ_buff/proof_gps.v
## Stack
theories/examples/stack/spec_na.v
theories/examples/stack/spec_per_elem.v
theories/examples/stack/event.v
theories/examples/stack/spec_graph.v
theories/examples/stack/code_na.v
theories/examples/stack/code_treiber.v
......
From stdpp Require Import countable.
Require Import iris.prelude.options.
(** Stack events *)
Inductive sevent := Push (v : Z) | Pop (v : Z) | EmpPop (* | FAIL_DEQ *).
Notation dummy_sevt := (Push 0).
Local Open Scope Z_scope.
Global Instance sevent_eq_dec : EqDecision sevent.
Proof. solve_decision. Defined.
Global Instance sevent_countable : Countable sevent.
Proof.
refine (
inj_countable'
(λ e, match e with
| Push v => (1, v)
| Pop v => (2, v)
| EmpPop => (3, 0) end)
(λ x, match x with
| (1, v) => Push v
| (2, v) => Pop v
| _ => EmpPop end) _);
by intros [].
Qed.
Definition is_push e v : Prop := e = Push v.
Definition is_pop e v : Prop := e = Pop v.
Definition is_maybe_pop e : Prop :=
match e with | Push _ => False | _ => True end.
From stdpp Require Import namespaces.
From iris.bi Require Import lib.fractional.
From gpfsl.logic Require Import logatom.
From gpfsl.examples.graph Require Export spec.
From gpfsl.examples.stack Require Export event.
Require Import iris.prelude.options.
Local Open Scope Z_scope.
(** Stack events *)
Inductive sevent := Push (v : Z) | Pop (v : Z) | EmpPop (* | FAIL_DEQ *).
Notation dummy_sevt := (Push 0).
Instance sevent_eq_dec : EqDecision sevent.
Proof. solve_decision. Defined.
Instance sevent_countable : Countable sevent.
Proof.
refine (
inj_countable'
(λ e, match e with
| Push v => (1, v)
| Pop v => (2, v)
| EmpPop => (3, 0) end)
(λ x, match x with
| (1, v) => Push v
| (2, v) => Pop v
| _ => EmpPop end) _);
by intros [].
Qed.
Local Notation graph := (graph sevent).
Local Notation event_list := (event_list sevent).
......@@ -41,11 +19,6 @@ Definition unmatched_push G eid : Prop :=
( id, (eid, id) G.(so)).
(** Stack predicates *)
Definition is_push e v : Prop := e = Push v.
Definition is_pop e v : Prop := e = Pop v.
Definition is_maybe_pop e : Prop :=
match e with | Push _ => False | _ => True end.
Local Notation EMPTY := 0 (only parsing).
Local Notation FAIL_RACE := (-1) (only parsing).
......
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