Issue with LTL Automizer

[kheradmand]

The following code breaks with nullPointerException in LTL Automizer's online interface.

//@ ltl invariant inv: [](AP(load_below_threshold == 1));

int load_below_threshold = 1;

void check_property(int* router_load){
    int p = 1;
    int i;
    for (i = 0; i < 4; i++){
        if (router_load[i] >= 3){
            p = 0; 
        } 
    }
    // if (router_load[0] < 3 && 
    // router_load[1] < 3 && 
    // router_load[2] < 3 && 
    // router_load[3] < 3){
    //     p = 1;
    // } else {
    //     p = 0;
    // }
    load_below_threshold = p;
}

int main(){
    int router_load[4] = {2,1,1,0};
    check_property(router_load);
    return 0;
}

But if I comment out the for loop and uncomment the if after that, it works.

[danieldietsch]

Thank you for your report!

Perhaps @Langenfeld can have a look, but it might take some time before someone can investigate.

[Langenfeld]

So, I tried to replicate the problem, and found that this only happens in the web interface.

For now using the binary version should be a good workaround, as I do not know when I am able to investigate the web interface problem.