salmans/rusty-razor

panics on hodor-time-loop example

salmans opened this issue · 1 comments

The following theory causes panic:

HoldTheDoor(t) -> Hodor(next(t));

Hodor(t) -> exists tt . HoldTheDoor(tt) & After(t, tt);

next(t0) = t1 -> After(t0, t1);
After(t0, t1) -> (next(t0) = t1) | exists t2 . next(t0) = t2 & After(t2, t1);

// Hold the door moment only happens at 't_hodor
HoldTheDoor(t) -> t = 't_hodor;
Hodor('t_hodor);

error:

thread 'main' panicked at 'called `Option::unwrap()` on a `None` value', libcore/option.rs:355:21
stack backtrace:
   0: std::sys::unix::backtrace::tracing::imp::unwind_backtrace
   1: std::sys_common::backtrace::print
   2: std::panicking::default_hook::{{closure}}
   3: std::panicking::default_hook
   4: std::panicking::rust_panic_with_hook
   5: std::panicking::continue_panic_fmt
   6: rust_begin_unwind
   7: core::panicking::panic_fmt
   8: core::panicking::panic
   9: rusty_razor::chase::impl::reference::Model::record
  10: <core::iter::Map<I, F> as core::iter::iterator::Iterator>::fold
  11: <alloc::vec::Vec<T> as alloc::vec::SpecExtend<T, I>>::from_iter
  12: rusty_razor::chase::impl::reference::Model::record
  13: <core::iter::Map<I, F> as core::iter::iterator::Iterator>::fold
  14: <alloc::vec::Vec<T> as alloc::vec::SpecExtend<T, I>>::from_iter
  15: <rusty_razor::chase::impl::reference::Model as rusty_razor::chase::ModelTrait>::observe
  16: <core::iter::FilterMap<I, F> as core::iter::iterator::Iterator>::next
  17: <alloc::vec::Vec<T> as alloc::vec::SpecExtend<T, I>>::from_iter
  18: <rusty_razor::chase::impl::reference::Evaluator as rusty_razor::chase::EvaluatorTrait<'s, Sel, B>>::evaluate
  19: rusty_razor::chase::solve
  20: razor::main
  21: std::rt::lang_start::{{closure}}
  22: std::panicking::try::do_call
  23: __rust_maybe_catch_panic
  24: std::rt::lang_start_internal
  25: main

A minimal example:

?x . P(x);
?x . Q(x);

P(x) & Q(y) -> x = y & P(x, y);

When facts are added on the rhs of the same sequent using reference implementation, the second fact points to a non-existing element that has already been identified with another element.