Skip to content

Commit

Permalink
Started writing tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@mortenhaahr
mortenhaahr committed Dec 3, 2024
1 parent c3ee948 commit cda0c1d
Show file tree
Hide file tree
Showing 2 changed files with 147 additions and 68 deletions.
154 changes: 120 additions & 34 deletions tests/constraint_based_lola.rs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
// Test untimed monitoring of LOLA specifications with the async runtime

use futures::stream::StreamExt;
use trustworthiness_checker::constraint_solver::ConstraintStore;
use std::collections::BTreeMap;
use trustworthiness_checker::constraint_based_runtime::ConstraintBasedMonitor;
use trustworthiness_checker::lola_specification;
Expand Down Expand Up @@ -34,84 +35,169 @@ async fn test_simple_add_monitor() {
);
}

#[ignore = "currently we can't handle recursive constraints in the solver as need a way to handle the inner indexes"]
fn env_len_assertions(env: &ConstraintStore, i_len: usize, r_len: usize, u_len: usize) {
fn nested_map_len<T1, T2>(map: &BTreeMap<T1, Vec<T2>>) -> usize {
let mut s = 0;
for (_, inner) in map {
s += inner.len();
}
s
}
assert_eq!(nested_map_len(&env.input_streams), i_len);
assert_eq!(nested_map_len(&env.outputs_resolved), r_len);
assert_eq!(nested_map_len(&env.outputs_unresolved), u_len);
}

#[ignore = "Cannot have empty spec or inputs"]
async fn test_runtime_initialization() {
let mut input_streams = input_empty();
let spec = lola_specification(&mut spec_empty()).unwrap();
let mut monitor = ConstraintBasedMonitor::new(spec, &mut input_streams);
let outputs: Vec< BTreeMap<VarName, Value>> = monitor.monitor_outputs().collect().await;
assert_eq!(outputs.len(), 0);
}

#[tokio::test]
async fn test_count_monitor() {
async fn test_var() {
let mut input_streams = input_streams1();
let spec = lola_specification(&mut spec_count_monitor()).unwrap();
let mut spec = "in x\nout z\nz =x";
let spec = lola_specification(&mut spec).unwrap();
let mut monitor = ConstraintBasedMonitor::new(spec, &mut input_streams);
let outputs: Vec<(usize, BTreeMap<VarName, Value>)> = monitor
.monitor_outputs()
.take(5)
.enumerate()
.collect()
.await;
let outputs: Vec<(usize, BTreeMap<VarName, Value>)> =
monitor.monitor_outputs().enumerate().collect().await;
assert!(outputs.len() == 2);
assert_eq!(
outputs,
vec![
(
0,
vec![(VarName("x".into()), Value::Int(1))]
vec![(VarName("z".into()), Value::Int(1))]
.into_iter()
.collect(),
),
(
1,
vec![(VarName("x".into()), Value::Int(2))]
vec![(VarName("z".into()), Value::Int(3))]
.into_iter()
.collect(),
),
]
);
}

#[tokio::test]
async fn test_literal_expression() {
// NOTE: This test makes less sense with async RV
let mut input_streams = input_streams1();
let mut spec = "in x\nout z\nz =42+x-x";
let spec = lola_specification(&mut spec).unwrap();
let mut monitor = ConstraintBasedMonitor::new(spec, &mut input_streams);
let outputs: Vec<(usize, BTreeMap<VarName, Value>)> =
monitor.monitor_outputs().enumerate().collect().await;
assert!(outputs.len() == 2);
assert_eq!(
outputs,
vec![
(
0,
vec![(VarName("z".into()), Value::Int(42))]
.into_iter()
.collect(),
),
(
1,
vec![(VarName("z".into()), Value::Int(42))]
.into_iter()
.collect(),
),
]
);
}

#[tokio::test]
async fn test_addition() {
let mut input_streams = input_streams1();
let mut spec = "in x\nout z\nz =x+1";
let spec = lola_specification(&mut spec).unwrap();
let mut monitor = ConstraintBasedMonitor::new(spec, &mut input_streams);
let outputs: Vec<(usize, BTreeMap<VarName, Value>)> =
monitor.monitor_outputs().enumerate().collect().await;
assert!(outputs.len() == 2);
assert_eq!(
outputs,
vec![
(
0,
vec![(VarName("z".into()), Value::Int(2))]
.into_iter()
.collect(),
),
(
2,
vec![(VarName("x".into()), Value::Int(3))]
1,
vec![(VarName("z".into()), Value::Int(4))]
.into_iter()
.collect(),
),
]
);
}

#[tokio::test]
async fn test_subtraction() {
let mut input_streams = input_streams1();
let mut spec = "in x\nout z\nz =x-10";
let spec = lola_specification(&mut spec).unwrap();
let mut monitor = ConstraintBasedMonitor::new(spec, &mut input_streams);
let outputs: Vec<(usize, BTreeMap<VarName, Value>)> =
monitor.monitor_outputs().enumerate().collect().await;
assert!(outputs.len() == 2);
assert_eq!(
outputs,
vec![
(
3,
vec![(VarName("x".into()), Value::Int(4))]
0,
vec![(VarName("z".into()), Value::Int(-9))]
.into_iter()
.collect(),
),
(
4,
vec![(VarName("x".into()), Value::Int(5))]
1,
vec![(VarName("z".into()), Value::Int(-7))]
.into_iter()
.collect(),
),
]
);
}

#[ignore = "currently we can't handle recursive constraints in the solver as need a way to handle the inner indexes"]
#[tokio::test]
async fn test_eval_monitor() {
let mut input_streams = input_streams2();
let spec = lola_specification(&mut spec_eval_monitor()).unwrap();
async fn test_index_past() {
let mut input_streams = input_streams1();
let mut spec = "in x\nout z\nz =x[-1, 0]";
let spec = lola_specification(&mut spec).unwrap();
let mut monitor = ConstraintBasedMonitor::new(spec, &mut input_streams);
let outputs: Vec<(usize, BTreeMap<VarName, Value>)> =
monitor.monitor_outputs().enumerate().collect().await;
monitor.monitor_outputs().enumerate().collect().await;
assert!(outputs.len() == 2);
assert_eq!(
outputs,
vec![
(
// Resolved to default on first step
0,
vec![
(VarName("z".into()), Value::Int(3)),
(VarName("w".into()), Value::Int(3))
]
.into_iter()
.collect(),
vec![(VarName("z".into()), Value::Int(0))]
.into_iter()
.collect(),
),
(
// Resolving to previous value on second step
1,
vec![
(VarName("z".into()), Value::Int(7)),
(VarName("w".into()), Value::Int(7))
]
.into_iter()
.collect(),
vec![(VarName("z".into()), Value::Int(1))]
.into_iter()
.collect(),
),
]
);
}


61 changes: 27 additions & 34 deletions tests/lola_fixtures.rs
View file
Original file line number Diff line number Diff line change
@@ -1,25 +1,30 @@
use futures::stream;
use futures::stream::BoxStream;
use std::{collections::BTreeMap, pin::Pin};
use trustworthiness_checker::{Value, OutputStream, VarName};
use trustworthiness_checker::{OutputStream, Value, VarName};

// Dead code is allowed in this file since cargo does not correctly
// track when functions are used in tests.

#[allow(dead_code)]
pub fn input_empty() -> BTreeMap<VarName, BoxStream<'static, Value>> {
BTreeMap::new()
}

// TODO: Make the input streams have 3 values...

#[allow(dead_code)]
pub fn input_streams1() -> BTreeMap<VarName, BoxStream<'static, Value>> {
let mut input_streams = BTreeMap::new();
input_streams.insert(
VarName("x".into()),
Box::pin(stream::iter(
vec![Value::Int(1), Value::Int(3)].into_iter(),
)) as Pin<Box<dyn futures::Stream<Item = Value> + std::marker::Send>>,
Box::pin(stream::iter(vec![Value::Int(1), Value::Int(3)].into_iter()))
as Pin<Box<dyn futures::Stream<Item = Value> + std::marker::Send>>,
);
input_streams.insert(
VarName("y".into()),
Box::pin(stream::iter(
vec![Value::Int(2), Value::Int(4)].into_iter(),
)) as Pin<Box<dyn futures::Stream<Item = Value> + std::marker::Send>>,
Box::pin(stream::iter(vec![Value::Int(2), Value::Int(4)].into_iter()))
as Pin<Box<dyn futures::Stream<Item = Value> + std::marker::Send>>,
);
input_streams
}
Expand All @@ -29,24 +34,18 @@ pub fn input_streams2() -> BTreeMap<VarName, BoxStream<'static, Value>> {
let mut input_streams = BTreeMap::new();
input_streams.insert(
VarName("x".into()),
Box::pin(stream::iter(
vec![Value::Int(1), Value::Int(3)].into_iter(),
)) as Pin<Box<dyn futures::Stream<Item = Value> + std::marker::Send>>,
Box::pin(stream::iter(vec![Value::Int(1), Value::Int(3)].into_iter()))
as Pin<Box<dyn futures::Stream<Item = Value> + std::marker::Send>>,
);
input_streams.insert(
VarName("y".into()),
Box::pin(stream::iter(
vec![Value::Int(2), Value::Int(4)].into_iter(),
)) as Pin<Box<dyn futures::Stream<Item = Value> + std::marker::Send>>,
Box::pin(stream::iter(vec![Value::Int(2), Value::Int(4)].into_iter()))
as Pin<Box<dyn futures::Stream<Item = Value> + std::marker::Send>>,
);
input_streams.insert(
VarName("s".into()),
Box::pin(stream::iter(
vec![
Value::Str("x+y".to_string()),
Value::Str("x+y".to_string()),
]
.into_iter(),
vec![Value::Str("x+y".to_string()), Value::Str("x+y".to_string())].into_iter(),
)) as Pin<Box<dyn futures::Stream<Item = Value> + std::marker::Send>>,
);
input_streams
Expand All @@ -57,15 +56,12 @@ pub fn input_streams3() -> BTreeMap<VarName, OutputStream<Value>> {
let mut input_streams = BTreeMap::new();
input_streams.insert(
VarName("x".into()),
Box::pin(stream::iter(
vec![Value::Int(1), Value::Int(3)].into_iter(),
)) as OutputStream<Value>,
Box::pin(stream::iter(vec![Value::Int(1), Value::Int(3)].into_iter()))
as OutputStream<Value>,
);
input_streams.insert(
VarName("y".into()),
Box::pin(stream::iter(
vec![Value::Int(2), Value::Int(4)].into_iter(),
)),
Box::pin(stream::iter(vec![Value::Int(2), Value::Int(4)].into_iter())),
);
input_streams
}
Expand All @@ -76,26 +72,23 @@ pub fn input_streams4() -> BTreeMap<VarName, OutputStream<Value>> {
input_streams.insert(
VarName("x".into()),
Box::pin(stream::iter(
vec![
Value::Str("a".to_string()),
Value::Str("c".to_string()),
]
.into_iter(),
vec![Value::Str("a".to_string()), Value::Str("c".to_string())].into_iter(),
)) as OutputStream<Value>,
);
input_streams.insert(
VarName("y".into()),
Box::pin(stream::iter(
vec![
Value::Str("b".to_string()),
Value::Str("d".to_string()),
]
.into_iter(),
vec![Value::Str("b".to_string()), Value::Str("d".to_string())].into_iter(),
)),
);
input_streams
}

#[allow(dead_code)]
pub fn spec_empty() -> &'static str {
""
}

#[allow(dead_code)]
pub fn spec_simple_add_monitor() -> &'static str {
"in x\n\
Expand Down

0 comments on commit cda0c1d

Please sign in to comment.