ssvlab / dsverifier

DSVerifier - Digital Systems Verifier
http://dsverifier.org
Apache License 2.0
12 stars 4 forks source link

The closed-loop stability verification seems to be broken #29

Open lucasccordeiro opened 7 years ago

lucasccordeiro commented 7 years ago

@lennonchaves and @iurybessa: can you please take a look at this example:

Here is our discrete plant:

digital_system plant = {
        .b = { 0.25f, 0.5f, 0.25f, -5.7065E-10 },
        .b_uncertainty = { 0.0, 0.0, 0.0, 0.0 },
        .b_size = 4,
        .a = { 1.0f, 6.8455E-9, 3.3925E-17, -3.4667E-94 },
        .a_uncertainty = { 0.0, 0.0, 0.0, 0.0 },
        .a_size = 4,
};

Here are two possible digital controllers:

__trace_controller={ .den={ 0.0107421875, 0, 0, 0 }, .den_uncertainty={ 0, 0, 0, 0 }, .den_size=1, .num={ 0.087890625, 0.021484375, 0, 0 }, .num_uncertainty={ 0, 0, 0, 0 }, .num_size=2}

__trace_controller={ .den={ 0.48828125, 0, 0, 0 }, .den_uncertainty={ 0, 0, 0, 0 }, .den_size=1, .num={ 0.9375, 0.25, 0, 0 }, .num_uncertainty={ 0, 0, 0, 0 }, .num_size=2 }

If we check stability for this closed-loop systems, then DSVerifier says that they are unstable. However, if we check them with the eiginside script (from Iury), then MATLAB says that they are stable.

lucasccordeiro commented 7 years ago

Additional info: It seems that our series composition is broken for this particular example. If we inspect the counterexample, we have a completely wrong denominator if we compare to MATLAB:

DSVerifier:
ans_den[0l]=0.234375 
ans_den[1l]=0.0546875 
ans_den[2l]=0.029296875 
ans_den[3l]=0.00390624976716935634613037109375 
ans_den[4l]=-0.00000000023283064365386962890625 

ans_num[0l]=0.234375 
ans_num[1l]=0.53125 
ans_num[2l]=0.359375
ans_num[3l]=0.0624999995343387126922607421875 
ans_num[4l]=-0.00000000023283064365386962890625 
MATLAB:
>> C2

C2 =

  0.9375 z + 0.25
  ---------------
      0.4883

Sample time: 0.1 seconds
Discrete-time transfer function.

>> P

P =

     0.25 z^3 + 0.5 z^2 + 0.25 z - 5.706e-10
  ---------------------------------------------
  z^3 + 6.845e-09 z^2 + 3.392e-17 z - 3.467e-94

Sample time: 0.1 seconds
Discrete-time transfer function.

>> CS = series(C2,P)

CS =

  0.2344 z^4 + 0.5312 z^3 + 0.3594 z^2 + 0.0625 z - 1.427e-10
  -----------------------------------------------------------
     0.4883 z^3 + 3.343e-09 z^2 + 1.656e-17 z - 1.693e-94

Sample time: 0.1 seconds
Discrete-time transfer function.