ariadne-cps / release-1.0

Frozen 1.0 release of the Ariadne C++ framework for cyber-physical systems
http://www.ariadne-cps.org
GNU General Public License v3.0
0 stars 0 forks source link

TaylorModel::value() after reconditioning not working correctly #51

Open lgeretti opened 7 years ago

lgeretti commented 7 years ago

Originally reported by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)


Thee reconditioning routine makes the value() method return 0.

For example, on ariadne, the code

#!c++
    Precision64 dp;
    ThresholdSweeper<Float64> swp(dp,1e-16);
    ValidatedTaylorModel<Float64> original({ {{0,0,0,0},4.}, {{1,0,0,0},1e-1}, {{0,1,0,0},1e-2} }, 1e-4, swp);
    Array<SizeType> discarded_variables(1);
    discarded_variables[0] = 1;
    ValidatedTaylorModel<Float64> reconditioned=recondition(original,discarded_variables,2,0);

returns the following original and reconditioned models:

#!c++

TM[4]( 4.0000000000000000 +0.1000000000000000*s0 +0.0100000000000000*s1+/-0.001)
TM[5]( 4.0000000000000000 +0.1000000000000000*s0 +0.0101000000000000*s3+/-0.000)

which are clearly correct.

Doing the same on the stable repository using the code

#!c++
    TaylorModel original=TaylorModel(Expansion<Float>(4,3, 0,0,0,0,4., 1,0,0,0,1e-1, 0,1,0,0,1e-2), 1e-4);
    Array<uint> discarded_variables(1);
    discarded_variables[0] = 1;
    TaylorModel reconditioned=recondition(original,discarded_variables,2,0);

Instead returns the following:

#!c++

(4.000000e+00+1.000000e-01*x0+1.000000e-02*x1+/-1.000000e-04)
(1.010000e-02*x3+4.000000e+00+1.000000e-01*x0+/-0.000000e+00)

which is still correct, but the x3 term is at the beginning. This may be a hint as to the source of the problem.

For practical purposes I attach the implementation of the recondition method for TaylorModel, in the two repositories. They appear the same to me.


lgeretti commented 7 years ago

Original comment by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


Try a simple sort() first.

lgeretti commented 7 years ago

Original comment by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)


It seems this is the reason. The iterator in the stable branch gives the reversed order in respect to yours. What would be the quickest way to fix this?

lgeretti commented 7 years ago

Original comment by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


Taylor model (in the main repositiory) uses ReverseLexicographicIndexLess to sort and relies on writers of low-level code to maintain the sorted order. The new terms (I believe) should go at the beginning. If this is the sort used in stable, you can just use the function from main. Otherwise, either try first sort() and then unique(). Or fix the order in the code. You could write a SortedExpansion::check to see if the terms are properly sorted.

lgeretti commented 7 years ago

Original comment by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)


Already tried, using unique_sort(), and it gives me the zero TaylorModel.

lgeretti commented 7 years ago

Original comment by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


Try explicitly sorting the coefficients after the reconditioning.