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

Fix exchanger spec

parent 213f085b
......@@ -170,7 +170,7 @@ Record exchanger_piggyback_spec {Σ} `{!noprolG Σ, !inG Σ (graphR xchg_event)}
ExchangerLocalLite_Persistent :
γg x G M, Persistent (ExchangerLocalLite γg x G M);
ExchangerLocalLite_Timeless :
γg x G M, Persistent (ExchangerLocalLite γg x G M);
γg x G M, Timeless (ExchangerLocalLite γg x G M);
ExchangerLocalLite_graph_snap :
γg x G M, ExchangerLocalLite γg x G M graph_snap γg G M;
ExchangerLocalLite_from :
......
Supports Markdown
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