Problem with simulation both in VSCode and in the web app

[ploc]

Hi, we are having a strange behavior in simulation.

The variable internal shall follow this regular expression: true;false; true*

In this first case, we have two errors: none of the signals is valid. ok is not equal to internal in the simulation. And none of them corresponds to true;false; true*

node top_invalid (tick: bool) returns (ok:bool);
var internal:bool;
let
    ok = internal;
    internal = true -> pre (false -> pre true); 

tel

In this second case, we added a check about the validity of signal internal. We don't expect it to hold, but the presence of this check changes the simulation output. Here is looks valid. Both signals are equal, and their value is true;false; true*.

node top_valid (tick: bool) returns (ok:bool);
var internal:bool;
let
    ok = internal;
    
    internal = true -> pre (false -> pre true); 
    --!PROPERTY internal; -- this property is not 
    -- expected to be true, but relying on internal 
    -- in this property solves the simulation issue.
tel

In this third example, we changed the property to be valid, adding a "or true" term to the property. Again the simulation is corrupted.

node top_invalid2 (tick: bool) returns (ok:bool);
var internal:bool;
let
    ok = internal;
    
    internal = true -> pre (false -> pre true); 

    -- worse, adding a term to the property makes 
    -- the simulation of internal signal invalid.
    --!PROPERTY (internal or true); 
tel

What is wrong here? Did we put an invalid term in the file that makes the simulation engine to break ?

Suggestions are welcomed.

[daniel-larraz]

Thank you for reporting this bug. PR #1008 should fix the issue.

This problem affects version 2.0.0 of Kind 2. I could also reproduce the issue in version 1.1.0.

Versions 1.2.0 to 1.9.0 should work fine.

[ploc]

Thanks for the very fast answer and solution. I confirm that replacing the kind2 binary in VSCode by the one compiled from source with opam solves the issue.