资 源 简 介
C++ library for solving systems of linear constraints: inequalities equality and disequality. Current version is based on Fourier-Motzkin (FM) elimination for inequalities and Gaussian elimination for equality. Quantifiers “Forall” and “Exists” are allowed. Boolean connectivities "&" -and, "|" - or "~" - not. "<" "<=" ">" ">=" "=" - arithmetical inequalities.
The simplest formula for the solver might be:
```
Exists x (x > 0 & x < 3);
```
The solver simplifies such formula to "true".
The solver simplifies system of equalities using LU decomposition. For example:
```
x + y = 3 &
x - y = 1 ;
```
Gives
```
x = 2 & y = 1
```
Time-Triggered Protocol. 2 nodes model example:
```
Forall (d, p, c, p, newc, newp)
((
~((newc = ( -0.5*(c + d) - p) ) &
(newp = p + c + d) & ( -1 <= d) &
(d <= 1) & (-M <= p) & (p <= M) &
((1-M) <= p + c) & (p + c<= M - 1) &
(- M <= c) & (c <= M)) |/
((1 - M <= newp + newc) &
(newp + newc <= M - 1))) &
(M > 1)
);
```
This e
