use std::cell::{Cell, RefCell};
use std::future::poll_fn;
use std::rc::Rc;
use std::task::{Poll, Waker};
use interweave::{Object, ObjectID, Observer, Step, StepCx, Transition, World, explore};
#[derive(Clone, Copy)]
enum Op {
Inc,
Get,
}
struct Request {
transition: Transition,
waker: Waker,
op: Op,
result: Rc<Cell<Option<usize>>>,
}
#[derive(Default)]
struct Inner {
count: usize,
seq: usize,
requests: Vec<Request>,
history: Vec<(Transition, Op, usize)>,
}
#[derive(Clone)]
struct Counter {
id: ObjectID,
state: Rc<RefCell<Inner>>,
}
impl Counter {
fn new(id: ObjectID) -> Self {
Self {
id,
state: Rc::new(RefCell::new(Inner::default())),
}
}
async fn inc(&self) {
self.request(Op::Inc).await;
}
async fn get(&self) -> usize {
self.request(Op::Get).await
}
async fn request(&self, op: Op) -> usize {
let result = Rc::new(Cell::new(None));
let mut op = Some(op);
poll_fn(move |cx| {
if let Some(value) = result.get() {
return Poll::Ready(value);
}
if let Some(op) = op.take() {
self.register(op, cx.waker().clone(), Rc::clone(&result));
}
Poll::Pending
})
.await
}
fn register(&self, op: Op, waker: Waker, result: Rc<Cell<Option<usize>>>) {
let mut st = self.state.borrow_mut();
let transition = Transition::new(self.id, st.seq);
st.seq += 1;
st.requests.push(Request {
transition,
waker,
op,
result,
});
}
fn op_of(&self, t: Transition) -> Op {
let st = self.state.borrow();
st.requests
.iter()
.map(|r| (r.transition, r.op))
.chain(st.history.iter().map(|(tt, op, _)| (*tt, *op)))
.find(|(tt, _)| *tt == t)
.map(|(_, op)| op)
.expect("transition not registered on this counter")
}
}
impl Object for Counter {
fn apply(&mut self, t: Transition) {
let mut st = self.state.borrow_mut();
let i = st
.requests
.iter()
.position(|r| r.transition == t)
.expect("transition must be enabled");
let req = st.requests.remove(i);
let observed = st.count;
if let Op::Inc = req.op {
st.count += 1;
}
st.history.push((t, req.op, observed));
req.result.set(Some(observed));
req.waker.wake();
}
fn enabled(&self) -> Vec<Transition> {
self.state
.borrow()
.requests
.iter()
.map(|r| r.transition)
.collect()
}
fn label(&self, t: Transition) -> String {
let st = self.state.borrow();
let (_, op, observed) = st
.history
.iter()
.find(|(tt, _, _)| *tt == t)
.expect("label called on an unapplied transition");
match op {
Op::Inc => format!("inc ({observed} -> {})", observed + 1),
Op::Get => format!("get -> {observed}"),
}
}
fn depends(&self, t1: Transition, t2: Transition) -> bool {
!matches!((self.op_of(t1), self.op_of(t2)), (Op::Get, Op::Get))
}
}
fn program(world: &mut World) {
let counter = world.register("counter", Counter::new);
let (a, b, reader) = (counter.clone(), counter.clone(), counter);
world.spawn("inc-a", async move {
a.inc().await;
Ok(())
});
world.spawn("inc-b", async move {
b.inc().await;
Ok(())
});
world.spawn("reader", async move {
reader.get().await;
Ok(())
});
}
#[derive(Default)]
struct Traces(usize);
impl Observer for Traces {
fn step(&mut self, step: Step<'_>, cx: StepCx<'_, '_>) {
if matches!(step, Step::Visit) && cx.state().is_terminal() {
self.0 += 1;
}
}
}
fn main() {
let mut traces = Traces::default();
explore(&program, &mut traces).expect("the counter never fails");
println!("custom Counter: {} maximal interleavings", traces.0);
}