Skip to main content

exchanges_nondeterministic

vstd::resource::storage_protocol

Function exchanges_nondeterministic 

Source 
pub open spec fn exchanges_nondeterministic<K, V, P: Protocol<K, V>>(
    p1: P,
    s1: IMap<K, V>,
    new_values: ISet<(P, IMap<K, V>)>,
) -> bool
Expand description
{
    forall |q: P, t1: IMap<K, V>| {
        P::rel(P::op(p1, q), t1)
            ==> exists |p2: P, s2: IMap<K, V>, t2: IMap<K, V>| {
                &&& new_values.contains((p2, s2))
                &&& P::rel(P::op(p2, q), t2)
                &&& t1.dom().disjoint(s1.dom())
                &&& t2.dom().disjoint(s2.dom())
                &&& t1.union_prefer_right(s1) =~= t2.union_prefer_right(s2)

            }
    }
}