[SAL-HELP] question

[Dulce María Hernández Rojas]

I have a model with these variables:

 

State: TYPE = {inicio,de,c,dce,dc,dch,ch};

 

INPUT

   encender:       BOOLEAN,

   cerrar:               BOOLEAN,

   abrir:                  BOOLEAN,

   reset:                BOOLEAN,

   preparar:         BOOLEAN,

   cocinar:             BOOLEAN

 

OUTPUT

   state: State

 

LOCAL

   d:  BOOLEAN,

   h:  BOOLEAN,

   cc: BOOLEAN,

   e:  BOOLEAN

 

I execute it in this fashion:

 

$ sal-inf-bmc --preserve-tmp-files --disable-traceability --disable-cse
--show-var-mapping -d 2 horno.sal  prop

 

My question is:

 

Why does the generated formulation show integer variables?

(define x_0::bool)

(define x_1::bool)

(define x_2::bool)

(define x_3::bool)

(define x_4::bool)

(define x_5::bool)

(define x_6::bool)

(define x_7::int)

(define x_8::bool)

(define x_9::bool)

(define x_10::int)

 

These integer variables are useless to me. I need the formulation without
them because I am doing calculations on the Boolean ones.

 

Thank you very much.


-- 
No virus found in this outgoing message.
Checked by AVG Free Edition.
Version: 7.5.446 / Virus Database: 268.18.24/742 - Release Date: 01/04/2007
08:49 p.m.
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/sal-help/attachments/20070402/64cc1468/attachment.html