nasa-sw-vnv/cocosim

Automated Analysis Framework for Simulink/Stateflow models.

cocosim's Issues

Translation error: A Lustre node with 4 parameters is called with only 3 arguments

Trying to verify the attached Simulink model with Nasa compiler generates the following error:

<Log class="info" source="parse">kind2 v1.1.0</Log>
<Log class="error" source="parse" line="313" column="10">Index mismatch for input parameters</Log>
</Results>

After investigation the source of the error is first line here:

d_T1_1 = d_T1_163_000(0.0, __time_step, __nb_step);
d_T2_1 = d_T2_164_000(0.0, kind2_times(h2_1, 1.10) + kind2_times(T_1 - preT2_1, 0.20) + kind2_times(preT1_1 - preT2_1, 0.30), __time_step, __nb_step);

The right call should be:

d_T1_1 = d_T1_163_000(0.0, kind2_times(h1_1, 0.9 ) + kind2_times(T_1 - preT1_1, 0.30) + kind2_times(preT2_1 - preT1_1, 0.30), __time_step, __nb_step);
d_T2_1 = d_T2_164_000(0.0, kind2_times(h2_1, 1.10) + kind2_times(T_1 - preT2_1, 0.20) + kind2_times(preT1_1 - preT2_1, 0.30), __time_step, __nb_step);

system20.zip
2017b.zip

Cocosim install Problem

Hello，
At present, I still haven't solved the problem of importing requirements. I said before that it seems to re execute the dependency according to "scripts / install_cocosim_lib. M". Do I execute it according to the following or other methods?

However, there will be other problems in this implementation, as shown in the figure：
There is another problem. When I execute the pre-built module of lustrec in "linux/bin", there will be a problem of missing library files. Is this the key to solving the problem?
Executing start_cocosim in matlab prompts that YICES2 cannot be found, is it related to the import requirements?

distutils not found while installing cocosim on virtual machine

Hi,

I'm trying to install cocosim on a virtual machine running ubuntu 22.04. I downloaded the .zip file from here: https://github.com/NASA-SW-VnV/CoCoSim/releases/tag/v1.1

After extracting the files i run 'install_cocosim' from the command line and i receive this error:

vboxuser@Ubuntu:~/MATLAB/CoCoSim/scripts$ ./install_cocosim
==> Checking required dependencies
==> Found all required utilities
==> Checking for CMake
==> Found CMake 3.22.1
==> Checking for m4
==> Found m4 1.4.18
==> Checking for Python
==> Found Python 3.10.12, version too old, skipped
==> Found Python 3.10.12, version too old, skipped
install_tools: error: Missing required python module: distutils

Can you please explain this error to me? Do i need to have python to run cocosim in MATLAB?

If I run cocosim without completing this step, then none of the verifiers binaries get installed and im unable to do any verification.

Problems with disabled library links for CoCoSim blocks

I've recently been getting errors that seem to derive from disabled library links. For example, when trying to "Prove properties" from the CoCoSim/examples/contract/absolute.slx, I get the following error:

When I "Check Compatibility" I see the following:

Also, I see in the Simulink Library Browser two CoCoSim specification libraries, and when I try to grab a model from the first library, I get an error:

It appears these are all related to each other?

Does CoCoSim support Matlab 2020B

Hi,
I use 2020b, when I start the example, I could not find the CoCoSim tool, thanks

Calls to Z3 from MATLAB fail

Issue observed on Ubuntu 20.04 with Matlab 9.8.0.1323502 (R2020a) on commit 35e9bf3.

Symptoms:

When attempting to "Prove properties" of a CoCoSim .slx model, Matlab reports the following error:

(Error)[TOLUSTRE] Simulink To Lustre Syntax check has failed. The parsing error is the following:                                                                                                                  
...                                                                                                                                                                                                                
<Log class="warn" source="parse">Couldn't determine Z3 version</Log>

This error occurs in checkSyntaxError.m, when executing a variant of the following line:
[status, output] = system('kind2 --enable interpreter -xml example_PP.KIND2.lus --timeout 60 --z3_bin z3')

Executing the same exact command in a terminal produces no errors.

The same behavior is observed when directly calling Z3 from the terminal and MATLAB, i.e.:
Terminal:

$ z3 -h                                                                                                                                                                                                            
Z3 [version 4.8.10 - 64 bit].                                                                                                                                                                                      

Matlab:

>> [status, output] = system('z3 -h')                                                                                                                                                                              
output =                                                                                                                                                                                                           
                                                                                                                                                                                                                   
    'z3: /usr/local/MATLAB/R2020a/sys/os/glnxa64/libstdc++.so.6: version `GLIBCXX_3.4.26' not found (required by z3)                                                                                               
     '                                                                                                                                                                                                             

Cause:

TLDR: The MATLAB library /usr/local/MATLAB/R2020a/sys/os/glnxa64/libstdc++.so.6 is outdated and Z3 requires a more recent library (for example /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.28). See https://www.mathworks.com/matlabcentral/answers/329796-issue-with-libstdc-so-6 for more info.

Fix:

Start MATLAB from the terminal with the LD_PRELOAD flag:
LD_PRELOAD=/usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.28 /usr/local/MATLAB/R2020a/bin/matlab
This will load the more recent libstdc++.so instead of that provided by MATLAB.

Prove properties

Hi,
A counterexample was returned when checking the FRETISH specification with Cocosim, but the counter-example does not seem to prove that the property is violated. The following are the models, specifications, and corresponding counterexamples.

What is "CoCoSimSpecificationLibrary/Implies" used for?

Hello,

In Simulink's Library Browser, I see under "CoCoSim Specification Library" a colomn named "Implies" and it has "A, A==>B, B, Logical Operator, Logical Operator 1" inside it. Please see the screenshot in attachment.

I wonder what are these used for. Perhaps they are blocks of "Implies" and have been placed here by mistake?

Thanks,

Yu XIA

False negative on norm(x)

I'm getting a false negative when dealing with norms. I believe the problem is an inaccuracy when reasoning on sqrt() over reals. Attached files provide the case and the log output, but the summary is below.

Function:
y = norm(x)
where x is in R^2

Contract:
dotproduct(x,x) < 25 => y < 5

This fails with the following counter-example:
x = [-2.2227,4]
y = 5.0313

But the evaluation of "y" is incorrect. By digging through the log files, it looks like it's correctly evaluating the dot product, but subsequently calculates the square root incorrectly.

I'm not sure if this is an error with parsing .slx to .lus, or if its an error with Kind2.

norm_error.tar.gz

“depext unmet” during installation

HI，thank you all for your great work.
During installing Cocosim using ./install_CoCoSim, I met this error message "opam-depext unmet availability conditions, e.g. 'opam-version >= "2.0.0~beta5" & opam-version < "2.1"'. Is there any solution?

Thank you!

Reorder function calls in install_cocosim_lib (develop branch)

install_cocosim fails when trying to do a fresh install (0721fca), looks related to changing the function calls such that install_tools is now called BEFORE updateRepo, copyCoCoFiles, and copyExternalLibFiles, instead of AFTER. When calling install_tools before, it attempts to reference functions (such as display_msg) that aren't defined until the updateRepo, copyCoCoFiles, and copyExternalLibFiles are called.