2014-02-25 22:50:56,293 [logger] - Performing change scenarios: full details available from: http://www-users.cs.york.ac.uk/~raduc/IncrementalSMT 2014-02-25 22:50:56,297 [logger] - Performing compositional verifiation steps to obtain initial resolution of the system: 2014-02-25 22:50:56,334 [logger] - Step Number: 1 ;-------------------------------------------------------------------------------- ;flat Z3 specification of model: app2 (declare-const ez1 Int) (declare-const ez2 Int) (declare-const fz1 Int) (declare-const fz2 Int) ;flat Z3 specification of model: app2 ;flat Z3 specification of model: e (assert ( >= ez1 0 )) (assert ( >= ez2 0 )) (assert ( >= (+ ez2 ez1 ) 1 )) (assert ( <= (+ ez2 ez1 ) 20 )) ;flat Z3 specification of model: f (assert ( >= fz1 0 )) (assert ( >= fz2 0 )) (assert ( >= (+ fz2 fz1 ) 1 )) (assert ( <= (+ fz2 fz1 ) 20 )) ;-------------------------------------------------------------------------------- ;-------------------------------------------------------------------------------- ;flat Z3 specification of model: db2 (declare-const iz1 Int) (declare-const iz2 Int) (declare-const jz1 Int) (declare-const jz2 Int) ;flat Z3 specification of model: db2 ;flat Z3 specification of model: i (assert ( >= iz1 0 )) (assert ( >= iz2 0 )) (assert ( >= (+ iz2 iz1 ) 1 )) (assert ( <= (+ iz2 iz1 ) 20 )) ;flat Z3 specification of model: j (assert ( >= jz1 0 )) (assert ( >= jz2 0 )) (assert ( >= (+ jz2 jz1 ) 1 )) (assert ( <= (+ jz2 jz1 ) 20 )) ;-------------------------------------------------------------------------------- ; Equations belonging to component s (assert (and ( = ez2 fz2 ) (and ( = ez1 fz1 ) ))) (assert (and ( = ez2 iz2 ) (and ( = ez1 iz1 ) ))) (assert (and ( = iz2 jz2 ) (and ( = iz1 jz1 ) ))) 2014-02-25 22:50:56,347 [logger] - Step Number: 2;-------------------------------------------------------------------------------- ;flat Z3 specification of model: a (declare-const az1 Int) (declare-const az2 Int) ;flat Z3 specification of model: a (assert ( >= az1 0 )) (assert ( >= az2 0 )) (assert ( >= (+ az2 az1 ) 1 )) (assert ( <= (+ az2 az1 ) 20 )) (assert ( = (+ az2 az1 ) 10 )) ;-------------------------------------------------------------------------------- 2014-02-25 22:50:56,348 [logger] - Step Number: 3;-------------------------------------------------------------------------------- ;flat Z3 specification of model: b (declare-const bz1 Int) (declare-const bz2 Int) ;flat Z3 specification of model: b (assert ( >= bz1 0 )) (assert ( >= bz2 0 )) (assert ( >= (+ bz2 bz1 ) 1 )) (assert ( <= (+ bz2 bz1 ) 20 )) (assert ( = bz2 0 )) ;-------------------------------------------------------------------------------- 2014-02-25 22:50:56,350 [logger] - Step Number: 4;-------------------------------------------------------------------------------- ;flat Z3 specification of model: c (declare-const cz1 Int) (declare-const cz2 Int) ;flat Z3 specification of model: c (assert ( >= cz1 0 )) (assert ( >= cz2 0 )) (assert ( >= (+ cz2 cz1 ) 1 )) (assert ( <= (+ cz2 cz1 ) 20 )) ;-------------------------------------------------------------------------------- 2014-02-25 22:50:56,350 [logger] - Step Number: 5;-------------------------------------------------------------------------------- ;flat Z3 specification of model: d (declare-const dz1 Int) (declare-const dz2 Int) ;flat Z3 specification of model: d (assert ( >= dz1 0 )) (assert ( >= dz2 0 )) (assert ( >= (+ dz2 dz1 ) 1 )) (assert ( <= (+ dz2 dz1 ) 20 )) ;-------------------------------------------------------------------------------- 2014-02-25 22:50:56,351 [logger] - Step Number: 6;-------------------------------------------------------------------------------- ;flat Z3 specification of model: g (declare-const gz1 Int) (declare-const gz2 Int) ;flat Z3 specification of model: g (assert ( >= gz1 0 )) (assert ( >= gz2 0 )) (assert ( >= (+ gz2 gz1 ) 1 )) (assert ( <= (+ gz2 gz1 ) 20 )) ;-------------------------------------------------------------------------------- 2014-02-25 22:50:56,352 [logger] - Step Number: 7;-------------------------------------------------------------------------------- ;flat Z3 specification of model: h (declare-const hz1 Int) (declare-const hz2 Int) ;flat Z3 specification of model: h (assert ( >= hz1 0 )) (assert ( >= hz2 0 )) (assert ( >= (+ hz2 hz1 ) 1 )) (assert ( <= (+ hz2 hz1 ) 20 )) ;-------------------------------------------------------------------------------- 2014-02-25 22:50:56,354 [logger] - Compositional Solution: Time: 0.056 seconds az1=10 az2=0 bz1=1 bz2=0 cz1=0 cz2=1 dz1=1 dz2=0 ez1=0 ez2=1 fz1=0 fz2=1 gz1=1 gz2=0 hz1=1 hz2=0 iz1=0 iz2=1 jz1=0 jz2=1 2014-02-25 22:50:56,354 [logger] - Performing scenario Change 1: Suppose that a new sub-component K is added to the component app2 such that there must be at least 7 instances of K deployed and Requirement (6) must remain satisfied. 2014-02-25 22:50:56,355 [logger] - Update: sub-component: k 2014-02-25 22:50:56,359 [logger] - Step: 1 ;-------------------------------------------------------------------------------- ;flat Z3 specification of model: app2 (declare-const ez1 Int) (declare-const ez2 Int) (declare-const fz1 Int) (declare-const fz2 Int) (declare-const kz1 Int) (declare-const kz2 Int) ;flat Z3 specification of model: app2 ;flat Z3 specification of model: e (assert ( >= ez1 0 )) (assert ( >= ez2 0 )) (assert ( >= (+ ez2 ez1 ) 1 )) (assert ( <= (+ ez2 ez1 ) 20 )) ;flat Z3 specification of model: f (assert ( >= fz1 0 )) (assert ( >= fz2 0 )) (assert ( >= (+ fz2 fz1 ) 1 )) (assert ( <= (+ fz2 fz1 ) 20 )) ;flat Z3 specification of model: k (assert ( >= kz1 0 )) (assert ( >= kz2 0 )) (assert ( >= (+ kz2 kz1 ) 1 )) (assert ( <= (+ kz2 kz1 ) 20 )) (assert ( >= (+ kz2 kz1 ) 7 )) ;-------------------------------------------------------------------------------- ;-------------------------------------------------------------------------------- ;flat Z3 specification of model: db2 (declare-const iz1 Int) (declare-const iz2 Int) (declare-const jz1 Int) (declare-const jz2 Int) ;flat Z3 specification of model: db2 ;flat Z3 specification of model: i (assert ( >= iz1 0 )) (assert ( >= iz2 0 )) (assert ( >= (+ iz2 iz1 ) 1 )) (assert ( <= (+ iz2 iz1 ) 20 )) ;flat Z3 specification of model: j (assert ( >= jz1 0 )) (assert ( >= jz2 0 )) (assert ( >= (+ jz2 jz1 ) 1 )) (assert ( <= (+ jz2 jz1 ) 20 )) ;-------------------------------------------------------------------------------- ; Equations belonging to component s (assert (and ( = ez2 fz2 ) (and ( = ez1 fz1 ) ))) (assert (and ( = ez2 kz2 ) (and ( = ez1 kz1 ) ))) (assert (and ( = ez2 iz2 ) (and ( = ez1 iz1 ) ))) (assert (and ( = iz2 jz2 ) (and ( = iz1 jz1 ) ))) 2014-02-25 22:50:56,363 [logger] - Incremental re-resolution took 7 seconds 2014-02-25 22:50:56,363 [logger] - Time: 0.004 seconds az1=10 az2=0 bz1=1 bz2=0 cz1=0 cz2=1 dz1=1 dz2=0 ez1=0 ez2=7 fz1=0 fz2=7 gz1=1 gz2=0 hz1=1 hz2=0 iz1=0 iz2=7 jz1=0 jz2=7 kz1=0 kz2=7 2014-02-25 22:50:56,363 [logger] - Performing scenario Change 2: Suppose that the system has a new database component to be deployed, comprising 3 sub-components L,M,N such that each sub-component must be deployed on zone 2. 2014-02-25 22:50:56,366 [logger] - Update: component: db3 2014-02-25 22:50:56,370 [logger] - Step: 1;-------------------------------------------------------------------------------- ;flat Z3 specification of model: l (declare-const lz1 Int) (declare-const lz2 Int) ;flat Z3 specification of model: l (assert ( >= lz1 0 )) (assert ( >= lz2 0 )) (assert ( >= (+ lz2 lz1 ) 1 )) (assert ( <= (+ lz2 lz1 ) 20 )) (assert ( >= (+ (ite (> lz2 0) 1 0) (ite (> lz1 0) 1 0)) 2 )) ;-------------------------------------------------------------------------------- 2014-02-25 22:50:56,372 [logger] - Step: 2;-------------------------------------------------------------------------------- ;flat Z3 specification of model: m (declare-const mz1 Int) (declare-const mz2 Int) ;flat Z3 specification of model: m (assert ( >= mz1 0 )) (assert ( >= mz2 0 )) (assert ( >= (+ mz2 mz1 ) 1 )) (assert ( <= (+ mz2 mz1 ) 20 )) (assert ( >= (+ (ite (> mz2 0) 1 0) (ite (> mz1 0) 1 0)) 2 )) ;-------------------------------------------------------------------------------- 2014-02-25 22:50:56,373 [logger] - Step: 3;-------------------------------------------------------------------------------- ;flat Z3 specification of model: n (declare-const nz1 Int) (declare-const nz2 Int) ;flat Z3 specification of model: n (assert ( >= nz1 0 )) (assert ( >= nz2 0 )) (assert ( >= (+ nz2 nz1 ) 1 )) (assert ( <= (+ nz2 nz1 ) 20 )) (assert ( >= (+ (ite (> nz2 0) 1 0) (ite (> nz1 0) 1 0)) 2 )) ;-------------------------------------------------------------------------------- 2014-02-25 22:50:56,376 [logger] - Incremental re-resolution took 0.01 seconds 2014-02-25 22:50:56,376 [logger] - Time: 0.007 seconds az1=10 az2=0 bz1=1 bz2=0 cz1=0 cz2=1 dz1=1 dz2=0 ez1=0 ez2=7 fz1=0 fz2=7 gz1=1 gz2=0 hz1=1 hz2=0 iz1=0 iz2=7 jz1=0 jz2=7 kz1=0 kz2=7 lz1=1 lz2=1 mz1=1 mz2=1 nz1=1 nz2=1 2014-02-25 22:50:56,376 [logger] - Performing scenario Change 3: Suppose that the web component has an added requirement that all sub-components must be in the same zone 2014-02-25 22:50:56,377 [logger] - Update: component: web 2014-02-25 22:50:56,380 [logger] - Step: 1 ;-------------------------------------------------------------------------------- ;flat Z3 specification of model: a (declare-const az1 Int) (declare-const az2 Int) ;flat Z3 specification of model: a (assert ( >= az1 0 )) (assert ( >= az2 0 )) (assert ( >= (+ az2 az1 ) 1 )) (assert ( <= (+ az2 az1 ) 20 )) (assert ( = (+ az2 az1 ) 10 )) ;-------------------------------------------------------------------------------- ;-------------------------------------------------------------------------------- ;flat Z3 specification of model: b (declare-const bz1 Int) (declare-const bz2 Int) ;flat Z3 specification of model: b (assert ( >= bz1 0 )) (assert ( >= bz2 0 )) (assert ( >= (+ bz2 bz1 ) 1 )) (assert ( <= (+ bz2 bz1 ) 20 )) (assert ( = bz2 0 )) ;-------------------------------------------------------------------------------- ; Equations belonging to component web (assert ( = (+ az2 az1 ) (+ bz2 bz1 ) )) 2014-02-25 22:50:56,383 [logger] - Incremental re-resolution took 0.006 ms 2014-02-25 22:50:56,383 [logger] - Time: 0.003 seconds az1=0 az2=10 bz1=10 bz2=0 cz1=0 cz2=1 dz1=1 dz2=0 ez1=0 ez2=7 fz1=0 fz2=7 gz1=1 gz2=0 hz1=1 hz2=0 iz1=0 iz2=7 jz1=0 jz2=7 kz1=0 kz2=7 lz1=1 lz2=1 mz1=1 mz2=1 nz1=1 nz2=1 2014-02-25 22:50:56,383 [logger] - Performing scenario Change 4: Suppose that we add a requirement to the service that the web component must be identically distributed to app2 (and by extension db2) 2014-02-25 22:50:56,384 [logger] - Update: component: s 2014-02-25 22:50:56,389 [logger] - Step: 1 ;-------------------------------------------------------------------------------- ;flat Z3 specification of model: web (declare-const az1 Int) (declare-const az2 Int) (declare-const bz1 Int) (declare-const bz2 Int) ;flat Z3 specification of model: web (assert ( = (+ az2 az1 ) (+ bz2 bz1 ) )) ;flat Z3 specification of model: a (assert ( >= az1 0 )) (assert ( >= az2 0 )) (assert ( >= (+ az2 az1 ) 1 )) (assert ( <= (+ az2 az1 ) 20 )) (assert ( = (+ az2 az1 ) 10 )) ;flat Z3 specification of model: b (assert ( >= bz1 0 )) (assert ( >= bz2 0 )) (assert ( >= (+ bz2 bz1 ) 1 )) (assert ( <= (+ bz2 bz1 ) 20 )) (assert ( = bz2 0 )) ;-------------------------------------------------------------------------------- ;-------------------------------------------------------------------------------- ;flat Z3 specification of model: app2 (declare-const ez1 Int) (declare-const ez2 Int) (declare-const fz1 Int) (declare-const fz2 Int) (declare-const kz1 Int) (declare-const kz2 Int) ;flat Z3 specification of model: app2 ;flat Z3 specification of model: e (assert ( >= ez1 0 )) (assert ( >= ez2 0 )) (assert ( >= (+ ez2 ez1 ) 1 )) (assert ( <= (+ ez2 ez1 ) 20 )) ;flat Z3 specification of model: f (assert ( >= fz1 0 )) (assert ( >= fz2 0 )) (assert ( >= (+ fz2 fz1 ) 1 )) (assert ( <= (+ fz2 fz1 ) 20 )) ;flat Z3 specification of model: k (assert ( >= kz1 0 )) (assert ( >= kz2 0 )) (assert ( >= (+ kz2 kz1 ) 1 )) (assert ( <= (+ kz2 kz1 ) 20 )) (assert ( >= (+ kz2 kz1 ) 7 )) ;-------------------------------------------------------------------------------- ;-------------------------------------------------------------------------------- ;flat Z3 specification of model: db2 (declare-const iz1 Int) (declare-const iz2 Int) (declare-const jz1 Int) (declare-const jz2 Int) ;flat Z3 specification of model: db2 ;flat Z3 specification of model: i (assert ( >= iz1 0 )) (assert ( >= iz2 0 )) (assert ( >= (+ iz2 iz1 ) 1 )) (assert ( <= (+ iz2 iz1 ) 20 )) ;flat Z3 specification of model: j (assert ( >= jz1 0 )) (assert ( >= jz2 0 )) (assert ( >= (+ jz2 jz1 ) 1 )) (assert ( <= (+ jz2 jz1 ) 20 )) ;-------------------------------------------------------------------------------- ; Equations belonging to component s (assert (and ( = ez2 fz2 ) (and ( = ez1 fz1 ) ))) (assert (and ( = ez2 kz2 ) (and ( = ez1 kz1 ) ))) (assert (and ( = ez2 az2 ) (and ( = ez1 az1 ) ))) (assert (and ( = az2 bz2 ) (and ( = az1 bz1 ) ))) (assert (and ( = ez2 iz2 ) (and ( = ez1 iz1 ) ))) (assert (and ( = iz2 jz2 ) (and ( = iz1 jz1 ) ))) 2014-02-25 22:50:56,394 [logger] - Incremental re-resolution took 0.01 ms 2014-02-25 22:50:56,394 [logger] - Time: 0.006 seconds az1=10 az2=0 bz1=10 bz2=0 cz1=0 cz2=1 dz1=1 dz2=0 ez1=10 ez2=0 fz1=10 fz2=0 gz1=1 gz2=0 hz1=1 hz2=0 iz1=10 iz2=0 jz1=10 jz2=0 kz1=10 kz2=0 lz1=1 lz2=1 mz1=1 mz2=1 nz1=1 nz2=1