tla-rs 0.1.0

Rust implementation of the IronFleet verified distributed systems framework
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

#![allow(unused_imports)]
use builtin::*;
use builtin_macros::*;
use vstd::{modes::*, prelude::*, seq::*, *};

use crate::common::framework::environment_s::*;
use crate::common::native::io_s::*;

verus! {
    pub enum LockMessage{
        Transfer{transfer_epoch:int},
        Locked{locked_epoch:int},
        Invalid
    }

    pub type LockEnvironment = LEnvironment<AbstractEndPoint, LockMessage>;
    pub type LockPacket = LPacket<AbstractEndPoint, LockMessage>;
    pub type LockIo = LIoOp<AbstractEndPoint, LockMessage>;
}