uppaalmodelchecker / uppaal-libs Goto Github PK

View Code? Open in Web Editor NEW

1.0 3.0 3.0 103 KB

Dynamic libraries for Uppaal models

Home Page: https://docs.uppaal.org/language-reference/system-description/declarations/external-functions/

License: MIT License

CMake 42.14% Shell 9.54% C++ 45.72% C 0.54% Batchfile 2.05%

csv csv-export csv-import model-checking timed-automata uppaal verification

uppaal-libs's People

Contributors

Stargazers

Watchers

Forkers

petergjoel magoorden estherhkim

uppaal-libs's Issues

Fix compilation for Windows

The library uses CMake setup which should work out-of-the-box for any operating system.
Unfortunately error.cpp contains some functions which are available only on POSIX environment (does not work with VisualStudio on Windows), so one needs MinGW to compile for Windows.
This code needs to be fixed to be portable.

Then we need github actions to provide release files for all three OSes.

Segmentation fault compiling on macOS

When running the compile script for the library on macOS, I get eventually a segmentation fault when running the tests. The full output of the compile script:

mgoorden@AAU121140 uppaal-libs % ./compile.sh
Expected a target platform as an argument. The following are supported:
    i686-w64-mingw32
    linux32-gcc10
    linux32-gcc11
    linux32-gcc12
    linux32
    linux64-gcc10
    linux64-gcc11
    linux64-gcc12
    linux64
    macos64-brew-gcc10
    macos64-brew-gcc11
    macos64-brew-gcc12
    macos64-ports-gcc10
    macos64-ports-gcc11
    macos64-ports-gcc12
    macos64
    x86_64-w64-mingw32

Guessing target platform(s):
     macos64 macos64-brew-gcc12
Configuring debug build for macos64
-- The C compiler identification is AppleClang 14.0.3.14030022
-- The CXX compiler identification is AppleClang 14.0.3.14030022
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- No extra warnings for AppleClang compiler
-- Enabled Undefined Behavior Sanitizer
-- Enabled Address Sanitizer
-- Configuring done
-- Generating done
-- Build files have been written to: /Users/mgoorden/Documents/uppaal-libs/build-macos64-debug
Building debug configuration for macos64
[8/8] Linking CXX executable src/test_table
Testing debug configuration for macos64
Test project /Users/mgoorden/Documents/uppaal-libs/build-macos64-debug
    Start 1: test_table
    Start 2: test_errors
1/2 Test #2: test_errors ......................   Passed    0.65 sec
2/2 Test #1: test_table .......................   Passed    1.36 sec

100% tests passed, 0 tests failed out of 2

Total Test time (real) =   1.36 sec
Configuring optimized release build for macos64
-- The C compiler identification is AppleClang 14.0.3.14030022
-- The CXX compiler identification is AppleClang 14.0.3.14030022
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- No extra warnings for AppleClang compiler
-- Configuring done
-- Generating done
-- Build files have been written to: /Users/mgoorden/Documents/uppaal-libs/build-macos64-release
Building optimized release configuration for macos64
[6/6] Linking CXX executable src/test_table
Testing optimized release configuration for macos64
Test project /Users/mgoorden/Documents/uppaal-libs/build-macos64-release
    Start 1: test_table
1/1 Test #1: test_table .......................   Passed    0.32 sec

100% tests passed, 0 tests failed out of 1

Total Test time (real) =   0.32 sec
Configuring debug build for macos64-brew-gcc12
-- The C compiler identification is GNU 12.2.0
-- The CXX compiler identification is GNU 12.2.0
-- Checking whether C compiler has -isysroot
-- Checking whether C compiler has -isysroot - yes
-- Checking whether C compiler supports OSX deployment target flag
-- Checking whether C compiler supports OSX deployment target flag - yes
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/local/bin/gcc-12 - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Checking whether CXX compiler has -isysroot
-- Checking whether CXX compiler has -isysroot - yes
-- Checking whether CXX compiler supports OSX deployment target flag
-- Checking whether CXX compiler supports OSX deployment target flag - yes
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/local/bin/g++-12 - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Extra warnings for GNU compiler
-- Enabled Undefined Behavior Sanitizer
-- Enabled Address Sanitizer
-- Configuring done
-- Generating done
-- Build files have been written to: /Users/mgoorden/Documents/uppaal-libs/build-macos64-brew-gcc12-debug
Building debug configuration for macos64-brew-gcc12
[2/8] Building CXX object src/CMakeFiles/errors.dir/errors.cpp.o
In file included from /Users/mgoorden/Documents/uppaal-libs/src/errors.cpp:5:
/Users/mgoorden/Documents/uppaal-libs/src/errors.hpp:16:60: warning: __VA_OPT__ is not available until C++20
   16 |         log_error(__FUNCTION__, __FILE__, __LINE__, format __VA_OPT__(, ) __VA_ARGS__)
      |                                                            ^
[3/8] Building CXX object src/CMakeFiles/table.dir/table.cpp.o
In file included from /Users/mgoorden/Documents/uppaal-libs/src/table.cpp:6:
/Users/mgoorden/Documents/uppaal-libs/src/errors.hpp:16:60: warning: __VA_OPT__ is not available until C++20
   16 |         log_error(__FUNCTION__, __FILE__, __LINE__, format __VA_OPT__(, ) __VA_ARGS__)
      |                                                            ^
[5/8] Building CXX object src/CMakeFiles/test_errors.dir/test_errors.cpp.o
In file included from /Users/mgoorden/Documents/uppaal-libs/src/test_errors.cpp:1:
/Users/mgoorden/Documents/uppaal-libs/src/errors.hpp:16:60: warning: __VA_OPT__ is not available until C++20
   16 |         log_error(__FUNCTION__, __FILE__, __LINE__, format __VA_OPT__(, ) __VA_ARGS__)
      |                                                            ^
[8/8] Linking CXX executable src/test_table
Testing debug configuration for macos64-brew-gcc12
Test project /Users/mgoorden/Documents/uppaal-libs/build-macos64-brew-gcc12-debug
    Start 1: test_table
    Start 2: test_errors
1/2 Test #1: test_table .......................***Exception: SegFault  0.48 sec

2/2 Test #2: test_errors ......................***Exception: SegFault  0.47 sec


0% tests passed, 2 tests failed out of 2

Total Test time (real) =   0.48 sec

The following tests FAILED:
      1 - test_table (SEGFAULT)
      2 - test_errors (SEGFAULT)
Errors while running CTest

Specify the separator

Currently, I guess, anything that is not a digit or a . is considered to be a column separator. It would be nice to specify what the column separator is for a particular file.

For example, I have a data file that looks like

0	10/05/2021	17:00:00	28.047283641646498	28.229890823364258	0.16600261628627777
1	10/05/2021	17:05:00	27.85280887167062	28.241891860961914	0.16254563629627228
2	10/05/2021	17:10:00	27.988941210653625	28.097787857055664	0.13076160848140717
3	10/05/2021	17:15:00	27.891703825665818	27.795202255249023	0.1424412727355957
....

where the actual columns are separated by the tab character. Right now, the library interprets the tab, /, and : as column separators. So the last column can be retrieved using column index 9, while intuitively (i.e., when you can specify that the tab is the separator) it has column index 5.

Syntax error after importing lib

I downloaded the compiled libtable.so and table.xml into the same folder.

Then I opened table.xml using uppaal and it prompted me with a syntax error.

UPPAAL version: 4.1.26-1

Strange simulator behavior when external function calls have side effects

hi.
I have tested the functionality of external function on UPPAAL-5 with the following code:

The source code of libexternal.so is as follows:

#include <cmath>

static int number = 42; // internal state, be careful

#ifdef __cplusplus
extern "C" { // tells C++ compiler to use C symbol name mangling (C compiler ignores)
#endif // __cplusplus

int get_number()
{   // is not free from side-effects, when set_number is used
    return number++;
}

#ifdef __cplusplus
} // end of "C" symbol name mangling
#endif // __cplusplus

The UPPAAL model is as follows:

When I use this model for symbolic simulation, it gives me values for the variable a that do not match the expectations.
It doesn't return number++ each time as defined by the get_number function, it actually increases number by 3 each time.

My complete model file is below:

test.xml.txt

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.