Suggestions on input format

[aman-goel]

I am thankful to the contributors for the wonderful work they have done. I have found the format useful (and simple) to extend SMT2 format to state transition systems (finite and infinite). I would like to suggest a few syntax changes/extensions to the .mcmt format.

1. Is there any specific reason why the keyword "define-state-type" has been used? Since the format allows definition of state variables as well as input variables, I would suggest either splitting state and input declarations separately. Example:

(define-state-type states  (x Real) (y Real))
(define-input-type inputs  (d Real))

Another alternative is to use keyword "define-type" instead of "define-state-type" (to avoid splitting) and possible confusion).

2. What's the reason for using state.x (for present state variable) when describing the transition relation? It is completely understood that next.x is needed to represent the next state variable versions. Moreover, the syntax state.x is not globally followed in the format (for example when defining a state formula, x is used directly).

3. The format looks simple (and useful) enough to extend for finite state transition systems, by borrowing syntax from QF_BV theory of SMT2 format. Here is an example of a finite version of example.mcmt. Any comment/suggestion would be appreciated.

;; Define Constants
(define-constant K0 (_ bv0 32))
(define-constant K1 (_ bv1 32))
(define-constant K19 (_ bv19 32))
(define-constant K20 (_ bv20 32))

;; A definition of a state type called "my_state_type" with variables
;; x and y of type (_ BitVec 32). 
(define-state-type my_state_type 
  ((x (_ BitVec 32)) (y (_ BitVec 32)))
)

;; Definition of a set of states "x_is_zero" capturing all states 
;; over the state type "my_state_type" where x is 0.
(define-states x_is_zero my_state_type
  (= x K0)
)

;; A definition of a set of states "initial_states" over 
;; "my_state_type" by a state formula. These are all states where 
;; both x and y are 0.
(define-states initial_states my_state_type
  (and x_is_zero (= y K0))
)

;; Definition of a transition where the next value of x is the 
;; current value + 1.
(define-transition inc_x my_state_type
  (= next.x (bvadd state.x K1))
)   

;; Definition of a transition that increases both x and y
(define-transition inc_x_and_y my_state_type
  (and inc_x (= next.y (bvadd state.y K1)))
)

;; Definition of a transition that increases x and y if not 
;; exceeding 20, or goes back to the state with x = y = 0
(define-transition transition my_state_type
  (or 
(and (bvult state.x K20) inc_x_and_y)
next.initial_states
  ) 
)

;; Directly define a simple counter system that increases x and y
(define-transition-system T1 my_state_type
   ;; Initial states 
   (and (= x K0) (= y K0))
   ;; Transition 
   (and (= next.x (bvadd state.x K1)) (= next.y (bvadd state.y K1)))
)

;; Define a counter system that can reset to 0 by reusing defined
;; formulas 
(define-transition-system T2 my_state_type
   ;; Initial states
   initial_states
   ;; Transitions 
   transition
)

;; Check whether x = y in T1
(query T1 (= x y))

;; Check whether x, y >= 0
(query T1 (and (bvuge x K0) (bvuge y K0)))

;; Check whether x, y <= 20
(query T2 (and (bvule x K20) (bvule y K20)))

;; Check whether x, y <= 19
(query T2 (and (bvule x K19) (bvule y K19)))

;; State type with inputs 
(define-state-type state_type_with_inputs
  ((x (_ BitVec 32)) (y (_ BitVec 32)))
  ((d (_ BitVec 32))) 
)

;; Transition system with inputs 
(define-transition-system T3 state_type_with_inputs
  (and (= x K0) (= y K0))
  (and (= next.x (bvadd state.x input.d))
   (= next.y (bvadd state.y input.d))
  )
) 

;; Check whether we're always the same 
(query T3 (= x y)) 

[BrunoDutertre]

Thanks for the comments @aman-goel! We're a bit busy with other
things right now so it may take a while before we digest it all. Hope
you find sally useful.