logic-rs
========
This library implements propositional and temporal logic in Rust. The objective is to enable both satisfaction and
robustness analysis of formulas using the provided operators. The architecture is intended to be extensible in order to
enable users to define custom logical operators for their own use cases.

Basic Usage
--------
This library allows users to define logical formulas which can be evaluated in two different contexts, timed or untimed.
An untimed context is a singular valuation is provided to the formula while a timed context is a series of valuations 
annotated with time steps. Formula elements are separated into two categories. The first category are expressions, which 
return values when evaluated by themselves. The second category are operators, which operate on expressions or other 
operators and do not return any value by themselves.

The currently provided expressions are:
- Predicates
- Propositions

The currently provided operators are (_* denotes a timed-only operator_):
- Not
- And
- Or
- Implies
- Next*
- Always*
- Eventually*

All expressions are defined to operate on valuations represented by hashmaps. A proposition operates on hashmaps with
string keys and boolean values, while a proposition operates on hashmaps with string keys and floating point values. A
proposition evaluates to true if the variable it refers to is true. A predicate is true if the weighted sum of the
variables it refers to is less than its bound value. A bound value may be a constant value or another variable.
Propositions and predicates __cannot__ be used together in the same formula because they operate on different
valuation types.

```rust
let proposition = Proposition::new("a");
let valuation = HashMap::from([
    ("a".to_string(), true)
]);
proposition.satisfied_by(&valuation); //True

let weight_map = HashMap::from([
    ("x".to_string(), 1.0),
    ("y".to_string(), 1.5),
]);
let predicate = Predicate::new(weight_map, Bound::Constant(10.0));
let valuation = HashMap::from([
    ("x".to_string(), 2.0),
    ("y".to_string(), 3.0),
]);
predicate.satisfied_by(&valuation); // 1.0 * 2.0 + 1.5 * 3.0 <= 10.0 => True
```

Binary and unary operators are constructed in the following manner:

```rust
And::new(Proposition::new("a"), Proposition::new("a"));
Not::new(Proposition::new("a"));
```

Timed operators also have an additional bounded constructor:

```rust
Always::new_bounded((0.0, 5.0), Proposition::new("a"));
```

In order to evaluate timed formulas, a trace must be constructed from an iterator of tuples that contain the time and
state value.

```rust
let trace = Trace::from_iter([
    (0.0, HashMap::from([("a".to_string(), true)])),
]);

let formula = Always::new(Proposition::new("a"));
formula.satisfied_by(&trace); // True
```

Predicates and all operators also support the concept of robustness, which is a measure of how close a valuation or
trace came to evaluating to false. These semantics can be accessed using the `distance` method.

```rust
let trace = Trace::from_iter([
    (0.0, HashMap::from([("a".to_string(), 9.0)])),
]);

let weights = HashMap::from([("x".to_string(), 1.0)])
let predicate = Predicate::new(weights, Bound::Constant(10.0));
let formula = Always::new(predicate);
formula.distance(&trace); // 1.0
```

A negative robustness value indicates that the formula was not satisfied, while a positive robustness value indicates
that the formula was satisfied.

Acknowledgements
----------------
This library is built using the work done in the following papers:
- Fainekos, Georgios E., and George J. Pappas. “Robustness of Temporal Logic Specifications for Continuous-Time Signals.” Theoretical Computer Science, vol. 410, no. 42, Elsevier B.V, 2009, pp. 4262–91, https://doi.org/10.1016/j.tcs.2009.06.021.
- Nickovic, Dejan, and Tomoya Yamaguchi. RTAMT: Online Robustness Monitors from STL. 2020.