panics on hodor-time-loop example
salmans opened this issue · 1 comments
salmans commented
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
salmans commented
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.