About available first-order logic semantics. #65
Description
Does Sally support exists and forall operators? I tried a simple example but it throws parser error at the location of "exists".
(define-state-type my_state
((x Real) (y Real))
)
(define-states initial_states my_state
(and (= x 1) (= y 2))
)
(define-transition transition my_state
(and (= next.x (+ state.x 1)) (= next.y (+ state.y 2)))
)
(define-transition-system T my_state
;; Initial states
initial_states
;; Transition
transition
)
(query T (
exists
((z Real))
((and (> y z) (> z x)))
))