diff --git a/07_Astree/src/ab_filter.c b/07_Astree/src/ab_filter.c
index 45e6a289eb237fdc6a5c32280add2e31da5a1b83..0efdbd772a9ae2e161e1a8e6de0bcf0f9073afaf 100644
--- a/07_Astree/src/ab_filter.c
+++ b/07_Astree/src/ab_filter.c
@@ -26,15 +26,20 @@ void InitFilter(AB_State *FilterState)
void TransientFilterStep(AB_State *FilterState, float sensorValue)
{
- __ASTREE_known_fact(((FilterState->initializationStep >= 1) && (FilterState->initializationStep <= 4294967295)));
- __ASTREE_known_fact((-10.0f < sensorValue && sensorValue < 10.0f));
- __ASTREE_known_fact((-10.0f < FilterState->value && 10.0f > FilterState->value));
- __ASTREE_known_fact((FilterState->h == FilterState->h));
- __ASTREE_known_fact((FilterState->sampling_interval == FilterState->sampling_interval));
+ //__ASTREE_known_fact(((FilterState->initializationStep >= 1) && (FilterState->initializationStep <= 4294967295)));
+ //__ASTREE_known_fact((-10.0f < sensorValue && sensorValue < 10.0f));
+ //__ASTREE_known_fact((-10.0f < FilterState->value && 10.0f > FilterState->value));
+ //__ASTREE_known_fact((FilterState->h == FilterState->h));
+ //__ASTREE_known_fact((FilterState->sampling_interval == FilterState->sampling_interval));
+
+ __ASTREE_assert((FilterState->initializationStep != 0));
float alphaN = (float)(2.0f*(float)(2.0f*(float)FilterState->initializationStep + 1.0f));
alphaN = (float)(alphaN/((float)((float)FilterState->initializationStep + 2.0f)*(float)((float)FilterState->initializationStep + 1.0f)));
+
+ float betaN = (6.0f)/((float)(FilterState->initializationStep + 2.0f)*(float)(FilterState->initializationStep + 2.0f));
+
if(alphaN < FilterState->g)
{
FilterState->isTransient = false;
@@ -51,7 +56,7 @@ void TransientFilterStep(AB_State *FilterState, float sensorValue)
FilterState->initializationStep += 1;
__ASTREE_known_fact(((FilterState->initializationStep >= 2) && (FilterState->initializationStep <= 4294967295)));
-
+ __ASTREE_assert((FilterState->initializationStep != 0));
//Filtern mit float
float rk, dxk, xk;
@@ -59,8 +64,13 @@ void TransientFilterStep(AB_State *FilterState, float sensorValue)
rk = sensorValue - FilterState->value;
- dxk = (float)(FilterState->dvalue + (FilterState->h * rk)/FilterState->sampling_interval);
- xk = FilterState->value + FilterState->sampling_interval * dxk + FilterState->g * rk;
+
+ if(rk > sensorValue)
+ return;
+
+
+ dxk = (float)(FilterState->dvalue + (betaN * rk)/FilterState->sampling_interval);
+ xk = FilterState->value + FilterState->sampling_interval * dxk + alphaN * rk;
FilterState->value = xk;
FilterState->dvalue = dxk;
@@ -72,28 +82,50 @@ void TransientFilterStep(AB_State *FilterState, float sensorValue)
double FilterStep(AB_State *FilterState, float sensorValue)
{
- __ASTREE_known_fact(((FilterState->initializationStep >= 1) && (FilterState->initializationStep <= 4294967295)));
- __ASTREE_known_fact((-10.0f < sensorValue && sensorValue < 10.0f));
- __ASTREE_known_fact((-10.0f < FilterState->value && 10.0f > FilterState->value));
- __ASTREE_known_fact((FilterState->h == FilterState->h));
- __ASTREE_known_fact((FilterState->sampling_interval == FilterState->sampling_interval));
+ //__ASTREE_known_fact(((FilterState->initializationStep >= 1) && (FilterState->initializationStep <= 4294967295)));
+ //__ASTREE_known_fact((-10.0f < sensorValue && sensorValue < 10.0f));
+ //__ASTREE_known_fact((-10.0f < FilterState->value && 10.0f > FilterState->value));
+ //__ASTREE_known_fact((FilterState->h == FilterState->h));
+ //__ASTREE_known_fact((FilterState->sampling_interval == FilterState->sampling_interval));
- double rk, dxk, xk, dxk_1, xk_1;
+ double rk = 0, dxk = 0, xk = 0, dxk_1 = 0, xk_1 = 0, errorResult = 0;
dxk_1 = FilterState->dvalue;
xk_1 = FilterState->value;
rk = sensorValue - FilterState->value;
+
+ if(rk > sensorValue)
+ return;
+
dxk = (double)(dxk_1 + ((double)FilterState->h * rk)/(double)FilterState->sampling_interval);
xk = xk_1 + (double)FilterState->sampling_interval * dxk + (double)FilterState->g * rk;
- FilterState->value = (float)xk;
- FilterState->dvalue = (float)dxk;
- if((xk > 10)||(xk < -10))
+
+ __ASTREE_partition_control
+ if((xk > 10.0f)||(xk < -10.0f))
{
InitFilter(FilterState);
- return 0;
+ __ASTREE_known_fact((errorResult == 0));
+ return errorResult;
+ }
+
+ if(xk != xk) // NaN Test
+ {
+ __ASTREE_known_fact((errorResult == 0));
+ return errorResult;
+
}
+ __ASTREE_partition_merge(());
+ //__ASTREE_modify((xk; full_range));
+
+
+ FilterState->value = (float)xk;
+ FilterState->dvalue = (float)dxk;
+
+ __ASTREE_known_fact((-10.0f < xk && xk < 10.0f));
+ __ASTREE_known_fact((xk == xk));
return xk;
+
}
diff --git a/07_Astree/src/main.c b/07_Astree/src/main.c
index a8ed1bcaea1056f090dadba903829f37a19de3cb..c53af048b6e1fa7fcfefbe45994d86dba1d654e8 100644
--- a/07_Astree/src/main.c
+++ b/07_Astree/src/main.c
@@ -91,7 +91,8 @@ int main(void) {
Sensor bla;
AB_State FilterState;
- double FilterValue = 0;
+
+
bool bufferstatefull = false;
float value = 0;
@@ -108,13 +109,13 @@ int main(void) {
bool result = false;
# ifdef __ASTREE__
- __ASTREE_modify ((result));
- result = 0;
+ __ASTREE_modify ((result; full_range));
+ //result = 0;
// __ASTREE_known_fact (( buffer > -10.0f && buffer < 10.0f));
# else
result = sensor_init(&bla, "/home/cip/nf2015/fi40zera/vezs/vezs16-vorgabe/07_Astree/src/sensor.dat");
#endif
- __ASTREE_modify((result));
+
InitFilter(&FilterState);
int i = 0;
@@ -127,8 +128,8 @@ int main(void) {
for(int i = 0; i < 2000; i++)//while(bufferstatefull == false)
{
# ifdef __ASTREE__
- __ASTREE_modify ((buffer; [-10.0f,10.0f]));
- buffer = 0;
+ __ASTREE_modify ((buffer; full_range));
+ __ASTREE_known_fact((-10.0f < buffer && buffer < 10.0f));
// __ASTREE_known_fact (( buffer > -10.0f && buffer < 10.0f));
# else
@@ -136,31 +137,53 @@ int main(void) {
//if(buffer != buffer)
// break;
-
+ #endif
bufferstatefull = BufferWrite(buffer);
-#endif
+//
}
__ASTREE_unroll ((2000))
while(bufferstatefull == true)
{
+ double FilterValue = 0;
+ /*FIlter prueft auf diese Grenzfaelle! Astree ignoriert das irgendwie*/
+ __ASTREE_known_fact((-10.0f < FilterValue && FilterValue < 10.0f));
+ __ASTREE_known_fact((FilterValue == FilterValue));
+ __ASTREE_modify ((FilterValue; full_range));
+
bufferstatefull = BufferRead(&value);
//Einschwingen des Filters
- if(FilterState.isTransient == true)
+ //__ASTREE_partition_control
+
+ switch(FilterState.isTransient)
{
- TransientFilterStep(&FilterState, value);
- }
+ //if(FilterState.isTransient == true)
+ //{
+ case true:
+ {
+ TransientFilterStep(&FilterState, value);
+ break;
+ }
+ //}
//Normaler Filtermodus
- else
+ //else
+ case false:
{
+ FilterValue = 0;
+ //__ASTREE_modify ((FilterValue; full_range));
FilterValue = FilterStep(&FilterState, value);
+
+
if(FilterState.isTransient == true)
{
//FilterValue = 0;
}
+ break;
+ }
}
+ //__ASTREE_partition_merge(());
fprintf(write, "%i %f %f\r\n",i, value, FilterValue);//Value = sensor, result = filter
diff --git a/07_Astree/src/sensor.c b/07_Astree/src/sensor.c
index 9d1bbed558d7ad7f4631fa1b0459b0656dcb7815..55dfed71337c468fa9becb143530c7813236c8dc 100644
--- a/07_Astree/src/sensor.c
+++ b/07_Astree/src/sensor.c
@@ -16,29 +16,29 @@ bool x = false;
bool sensor_init(Sensor *sensor, const char *filename){
# ifdef __ASTREE__
- __ASTREE_modify ((x));
- x = false;
+ __ASTREE_modify ((x; full_range));
+ //x = false;
# else
- FILE *test = NULL;
- int i = 0;
-
- test = fopen(filename, "r");
-
- if(test != NULL)
- {
- sensor->file = test;
-
- while(fscanf(test, "%f;%f", &sensorArr[i], &sensorArr[i + 1]) == 2)
- {
- i += 2;
- }
-
- fclose(test);
- x = true;
- return x;
- }
- x = false;
- return x;
+ FILE *test = NULL;
+ int i = 0;
+
+ test = fopen(filename, "r");
+
+ if(test != NULL)
+ {
+ sensor->file = test;
+
+ while(fscanf(test, "%f;%f", &sensorArr[i], &sensorArr[i + 1]) == 2)
+ {
+ i += 2;
+ }
+
+ fclose(test);
+ x = true;
+ return x;
+ }
+ x = false;
+ return x;
#endif
}
@@ -52,8 +52,9 @@ bool sensor_init(Sensor *sensor, const char *filename){
float getSensorValue(void)
{
# ifdef __ASTREE__
- __ASTREE_modify ((buffer; [-10.0f,10.0f]));
- buffer = 0;
+ __ASTREE_modify ((buffer; full_range));
+ __ASTREE_known_fact((-10.0f < buffer && buffer < 10.0f));
+
// __ASTREE_known_fact (( buffer > -10.0f && buffer < 10.0f));
# else
buffer = sensorArr[counter];
@@ -65,6 +66,7 @@ float getSensorValue(void)
}
return buffer;
+
# endif
}