diff --git a/bats/symon.bats b/bats/symon.bats index a828bed..fc2a52a 100755 --- a/bats/symon.bats +++ b/bats/symon.bats @@ -51,6 +51,7 @@ assert_example_output() { @test "features" { readonly SPEC="${EXAMPLE_DIR}/features.symon" assert_example_output "-nf" "$SPEC" + assert_example_output "-bnf" "${EXAMPLE_DIR}/features2.symon" } @test "non-integer boolean" { @@ -67,6 +68,7 @@ assert_example_output() { @test "expr_assignment" { assert_example_output "-bnf" "${EXAMPLE_DIR}/expr_assignment.symon" + assert_example_output "-bnf" "${EXAMPLE_DIR}/expr_assignment2.symon" } @test "data parametric unobservable" { @@ -87,8 +89,17 @@ assert_example_output() { @test "boolean unobservable" { assert_example_output "-bnf" "${EXAMPLE_DIR}/unobservable_boolean.symon" + assert_example_output "-bnf" "${EXAMPLE_DIR}/unobservable2_boolean.symon" + assert_example_output "-dnf" "${EXAMPLE_DIR}/unobservable2_data_parametric.symon" } @test "decimal_inputs" { assert_example_output "-dnf" "${EXAMPLE_DIR}/decimal_inputs.symon" + assert_example_output "-dnf" "${EXAMPLE_DIR}/decimal_inputs2.symon" +} + +@test "decimal_time" { + assert_example_output "-bnf" "${EXAMPLE_DIR}/decimal_time_boolean.symon" + assert_example_output "-dnf" "${EXAMPLE_DIR}/decimal_time_data_parametric.symon" + assert_example_output "-pnf" "${EXAMPLE_DIR}/decimal_time_parametric.symon" } diff --git a/example/decimal_inputs2.symon b/example/decimal_inputs2.symon new file mode 100644 index 0000000..882d617 --- /dev/null +++ b/example/decimal_inputs2.symon @@ -0,0 +1,18 @@ +#!/usr/bin/env symon -dnf +## BEGIN_INPUT +# event 0 1 +# event 0.5 2 +# event 1 3 +# event 0.0625 4 +## END_INPUT +## BEGIN_OUTPUT +# @2.000000. (time-point 1) true +# @4.000000. (time-point 3) true +## END_OUTPUT + +signature event { + n: number; +} + +event()*; +event( x | 0 < x && x < 1 ) diff --git a/example/decimal_time_boolean.symon b/example/decimal_time_boolean.symon new file mode 100644 index 0000000..bc5aac7 --- /dev/null +++ b/example/decimal_time_boolean.symon @@ -0,0 +1,29 @@ +#!/usr/bin/env symon -bnf +## BEGIN_INPUT +# event a 0 +# event b 1.25 +# event c 2.6 +# event a 10 +# event b 10.85 +# event c 11.625 +## END_INPUT +## BEGIN_OUTPUT +# @11.625000. (time-point 5) +## END_OUTPUT + +signature event { + id: string; +} + +event()*; +event( id | id == "a"); +within (> 1.5) { + within (< 2.5) { + within (> 0.5) { + within (< 1.5) { + event( id | id == "b" ) + } + }; + event( id | id == "c" ) + } +} diff --git a/example/decimal_time_data_parametric.symon b/example/decimal_time_data_parametric.symon new file mode 100644 index 0000000..fa64d2c --- /dev/null +++ b/example/decimal_time_data_parametric.symon @@ -0,0 +1,29 @@ +#!/usr/bin/env symon -dnf +## BEGIN_INPUT +# event a 0 +# event b 1.25 +# event c 2.6 +# event a 10 +# event b 10.85 +# event c 11.625 +## END_INPUT +## BEGIN_OUTPUT +# @11.625000. (time-point 5) true +## END_OUTPUT + +signature event { + id: string; +} + +event()*; +event( id | id == "a"); +within (> 1.5) { + within (< 2.5) { + within (> 0.5) { + within (< 1.5) { + event( id | id == "b" ) + } + }; + event( id | id == "c" ) + } +} diff --git a/example/decimal_time_parametric.symon b/example/decimal_time_parametric.symon new file mode 100644 index 0000000..731fa2e --- /dev/null +++ b/example/decimal_time_parametric.symon @@ -0,0 +1,29 @@ +#!/usr/bin/env symon -pnf +## BEGIN_INPUT +# event a 0 +# event b 1.25 +# event c 2.6 +# event a 10 +# event b 10.85 +# event c 11.625 +## END_INPUT +## BEGIN_OUTPUT +# @11.625. (time-point 5) Num: true Clock: 8*A = 13 +## END_OUTPUT + +signature event { + id: string; +} + +event()*; +event( id | id == "a"); +within (> 1.5) { + within (< 2.5) { + within (> 0.5) { + within (< 1.5) { + event( id | id == "b" ) + } + }; + event( id | id == "c" ) + } +} diff --git a/example/expr_assignment2.symon b/example/expr_assignment2.symon new file mode 100644 index 0000000..78e7e4e --- /dev/null +++ b/example/expr_assignment2.symon @@ -0,0 +1,32 @@ +#!/usr/bin/env symon -dnf +## BEGIN_INPUT +# init 0 +# check 0 1 +# init 2 +# add 1 3 +# add 2 4 +# add 3 5 +# add 4 6 +# check 10 7 +## END_INPUT +## BEGIN_OUTPUT +# @1.000000. (time-point 1) x0 == 0 +# @7.000000. (time-point 7) x0 == 10 +## END_OUTPUT + +var { + v: number; +} + +signature init {} +signature add { + n: number; +} +signature check { + n: number; +} + +(init() || add() || check())*; +init( | | v := 0 ); +add( n | | v := n + 0 + v )*; +check( n | v = n ) diff --git a/example/features2.symon b/example/features2.symon new file mode 100644 index 0000000..22a5b1e --- /dev/null +++ b/example/features2.symon @@ -0,0 +1,13 @@ +#!/usr/bin/env symon -nf +## BEGIN_INPUT +# event 10 0.5 +## END_INPUT +## BEGIN_OUTPUT +# @0.500000. (time-point 0) +## END_OUTPUT + +signature event { + n: number; +} + +event( n | -1 + n < 0 + n + 1 ) diff --git a/example/unobservable2_boolean.symon b/example/unobservable2_boolean.symon new file mode 100644 index 0000000..9bfa6e0 --- /dev/null +++ b/example/unobservable2_boolean.symon @@ -0,0 +1,25 @@ +#!/usr/bin/env symon -bnf +## BEGIN_INPUT +# event a 0 +# event b 2 +# event a 10 +# event b 11 +## END_INPUT +## BEGIN_OUTPUT +# @2.000000. (time-point 1) x0 == z +## END_OUTPUT + +var { + value: string; +} + +signature event { + id: string; +} + +(event(id))*; +event( id | id == "a" | value := "x"); +within (= 2) { + unobservable(| | value := "z") +}; +event( id | id == "b" && value == "z") diff --git a/example/unobservable2_data_parametric.symon b/example/unobservable2_data_parametric.symon new file mode 100644 index 0000000..64b8af3 --- /dev/null +++ b/example/unobservable2_data_parametric.symon @@ -0,0 +1,25 @@ +#!/usr/bin/env symon -dnf +## BEGIN_INPUT +# event a 0 +# event b 2 +# event a 10 +# event b 11 +## END_INPUT +## BEGIN_OUTPUT +# @2.000000. (time-point 1) x0 == z true +## END_OUTPUT + +var { + value: string; +} + +signature event { + id: string; +} + +(event(id))*; +event( id | id == "a" | value := "x"); +within (= 2) { + unobservable(| | value := "z") +}; +event( id | id == "b" && value == "z")