use todc_utils::linearizability::WGLChecker;
use todc_utils::specifications::etcd::{history_from_log, EtcdSpecification};
type EtcdChecker = WGLChecker<EtcdSpecification>;
#[macro_export]
macro_rules! etcd_tests {
( $($name:ident: $values:expr,)* )=> {
$(
#[test]
fn $name() {
let (log_number, expected_result) = $values;
let history = history_from_log(
format!("tests/linearizability/etcd/etcd_{}.log", log_number)
);
let result = EtcdChecker::is_linearizable(history);
assert_eq!(result, expected_result);
}
)*
}
}
etcd_tests! {
test_000: ("000", false),
test_001: ("001", false),
test_002: ("002", true),
test_003: ("003", false),
test_004: ("004", false),
test_005: ("005", true),
test_006: ("006", false),
test_007: ("007", true),
test_008: ("008", false),
test_009: ("009", false),
test_010: ("010", false),
test_011: ("011", false),
test_012: ("012", false),
test_013: ("013", false),
test_014: ("014", false),
test_015: ("015", false),
test_016: ("016", false),
test_017: ("017", false),
test_018: ("018", true),
test_019: ("019", false),
test_020: ("020", false),
test_021: ("021", false),
test_022: ("022", false),
test_023: ("023", false),
test_024: ("024", false),
test_025: ("025", true),
test_026: ("026", false),
test_027: ("027", false),
test_028: ("028", false),
test_029: ("029", false),
test_030: ("030", false),
test_031: ("031", true),
test_032: ("032", false),
test_033: ("033", false),
test_034: ("034", false),
test_035: ("035", false),
test_036: ("036", false),
test_037: ("037", false),
test_038: ("038", true),
test_039: ("039", false),
test_040: ("040", false),
test_041: ("041", false),
test_042: ("042", false),
test_043: ("043", false),
test_044: ("044", false),
test_045: ("045", true),
test_046: ("046", false),
test_047: ("047", false),
test_048: ("048", true),
test_049: ("049", true),
test_050: ("050", false),
test_051: ("051", true),
test_052: ("052", false),
test_053: ("053", true),
test_054: ("054", false),
test_055: ("055", false),
test_056: ("056", true),
test_057: ("057", false),
test_058: ("058", false),
test_059: ("059", false),
test_060: ("060", false),
test_061: ("061", false),
test_062: ("062", false),
test_063: ("063", false),
test_064: ("064", false),
test_065: ("065", false),
test_066: ("066", false),
test_067: ("067", true),
test_068: ("068", false),
test_069: ("069", false),
test_070: ("070", false),
test_071: ("071", false),
test_072: ("072", false),
test_073: ("073", false),
test_074: ("074", false),
test_075: ("075", true),
test_076: ("076", true),
test_077: ("077", false),
test_078: ("078", false),
test_079: ("079", false),
test_080: ("080", true),
test_081: ("081", false),
test_082: ("082", false),
test_083: ("083", false),
test_084: ("084", false),
test_085: ("085", false),
test_086: ("086", false),
test_087: ("087", true),
test_088: ("088", false),
test_089: ("089", false),
test_090: ("090", false),
test_091: ("091", false),
test_092: ("092", true),
test_093: ("093", false),
test_094: ("094", false),
test_096: ("096", false),
test_097: ("097", false),
test_098: ("098", true),
test_099: ("099", false),
test_100: ("100", true),
test_101: ("101", true),
test_102: ("102", true),
}