Incorrect traces, depending on the order of queries

[yav]

This is with the version of Sally compiled again revision c9856e7a751eebf11e from GitHub.

Sally seems to be producing incorrect traces in some cases. Here is an example transitions system with two queries:

(define-state-type
   S
   (
     (p Int)
     (p_del Int)
     (p_nil Bool)
     (x Int)
     (x_del Int)
     (x_nil Bool)
     (y Int)
     (y_del Int)
     (y_nil Bool))
   ())
(define-transition-system
   TS
   S
   (and
      (= y x)
      (= y_del x_del)
      (= y_nil true)
      (=
         p
         (+ 1 y))
      (= p_del 0)
      (=
         p_nil
         (or false y_nil))
      (= 0 y_del)
      (= x 1)
      (= x_del 0)
      (= x_nil false))
   (and
      (= next.y state.x)
      (= next.y_del state.x_del)
      (= next.y_nil state.x_nil)
      (=
         next.p
         (+ 1 next.y))
      (= next.p_del 0)
      (=
         next.p_nil
         (or false next.y_nil))
      (= 0 next.y_del)
      (= next.x next.p)
      (= next.x_del next.p_del)
      (= next.x_nil next.p_nil)))
(query
   TS
   (= x 1))
(query
   TS
   (= x 2))

This produces the traces below, using flags: sally --engine=pdkind --show-trace

invalid
(trace 
  (state
    (p 2)
    (|p_del| 0)
    (|p_nil| true)
    (x 1)
    (|x_del| 0)
    (|x_nil| false)
    (y 1)
    (|y_del| 0)
    (|y_nil| true)
  )
  (input
  )
  (state
    (p 2)
    (|p_del| 0)
    (|p_nil| false)
    (x 2)
    (|x_del| 0)
    (|x_nil| false)
    (y 1)
    (|y_del| 0)
    (|y_nil| false)
  )
)

invalid
(trace 
  (state
    (p 2)
    (|p_del| 0)
    (|p_nil| true)
    (x 1)
    (|x_del| 0)
    (|x_nil| false)
    (y 1)
    (|y_del| 0)
    (|y_nil| true)
  )
  (input
  )
  (state
    (p 2)
    (|p_del| 0)
    (|p_nil| false)
    (x 2)
    (|x_del| 0)
    (|x_nil| false)
    (y 1)
    (|y_del| 0)
    (|y_nil| false)
  )
)

The first trace is the correct answer for query 1, however the second one appears to be just a copy of the first. Indeed, query 2 should fail with an empty trace, as it is already false in the initial state.

If I swap the order of the queries, then I get the expected answer.

[dddejan]

Thanks for the report. This was indeed a bug. It should be fixed, but let me know if there is more issues. We don't have many use-cases yet with multiple queries so I'm sure there is more bugs lurking.

As a note, for second query, the resulting trace is of size 1 (values in initial state).

[yav]

Thanks for the quick fix, it seems to work! Am I correct in a assuming that one should never get an empty trace, as the last state in the trace should be the one that violates the query?

It would seem that previously Sally would sometimes produce empty traces, but maybe it was related to this bug.