Yices input-files for A/G specification contain unrequired input
Consider the attached AF3-model. There are generated two *.ys, one for
each connection.
However, each file contains both guarantees of both sending components,
eaven if only one of those is required.
(bold texts are not required to do the analysis)
= GENERATED =
(define-type SIGNAL_TYPE (scalar Val NoVal ))
(define Output_10_SIGNAL :: SIGNAL_TYPE )
(define Output_10 :: int)
(define InputA_11_SIGNAL :: SIGNAL_TYPE )
(define InputA_11 :: int)
(assert
(and
(= Output10 InputA__11)
(= Output10_SIGNAL InputA__11_SIGNAL)
)
)
(assert
(not
(or
(not
(and
(and
true
(and
(>Output_10 10)
(= Output_10_SIGNAL Val)
)
)
(and
)
)
)
(and
(>InputA_11 10)
(= InputA_11_SIGNAL Val)
)
)
)
)
(check)
= ONLY REQUIRED =
(define-type SIGNAL_TYPE (scalar Val NoVal ))
(define Output_10_SIGNAL :: SIGNAL_TYPE )
(define Output_10 :: int)
(define InputA_11_SIGNAL :: SIGNAL_TYPE )
(define InputA_11 :: int)
(assert
(and
(= Output10 InputA__11)
(= Output10_SIGNAL InputA__11_SIGNAL)
)
)
(assert
(not
(or
(not
(and
(>Output_10 10)
(= Output_10_SIGNAL Val)
)
)
(and
(>InputA_11 10)
(= InputA_11_SIGNAL Val)
)
)
)
)
(check)
(from redmine: issue id 990, created on 2012-09-25, closed on 2018-01-29)
- Relations:
- parent #959 (closed)
- Uploads: