From 98c76f5104768167eee45670ad684861cc7b0d9e Mon Sep 17 00:00:00 2001 From: Tomaz Date: Wed, 1 May 2024 18:41:55 +0200 Subject: [PATCH] new test checking all syntatic transformations --- tests/regression_tests_data.py | 96 +++++++++++++++++++ .../{syntatic_check.imi => syntatic_test.imi} | 4 +- 2 files changed, 98 insertions(+), 2 deletions(-) rename tests/testcases/templates/{syntatic_check.imi => syntatic_test.imi} (88%) diff --git a/tests/regression_tests_data.py b/tests/regression_tests_data.py index 29cf6ef1..416fa386 100644 --- a/tests/regression_tests_data.py +++ b/tests/regression_tests_data.py @@ -28248,5 +28248,101 @@ }] } , + { + 'purpose' : 'Test each syntatic expansion implemented (templates, syntatic arrays, etc.)', + 'input_files' : ['templates/syntatic_test.imi'], + 'options' : '-verbose mute -imi2IMI', + 'expectations' : [{ + 'file' : 'syntatic_test-regenerated.imi', + 'content': """ +var + x___0, x___1 + : clock; + + id + : int; + + params___0, params___1 + : parameter; + + + +(************************************************************) + automaton p___0 +(************************************************************) + actions: acts___0; + +loc A: invariant params___0 >= x___0 + when id = -1 do {x___0 := 0;} sync acts___0 goto req; + +loc req: invariant 2 >= x___0 + when 2 >= x___0 do {x___0 := 0; id := 0;} (* sync nosync_1*) goto waiting; + +loc waiting: invariant True + when id = -1 do {x___0 := 0;} (* sync nosync_2*) goto req; + when id = 0 +& x___0 > 2 do {} (* sync nosync_3*) goto cs; + +loc cs: invariant True + when True do {id := -1;} (* sync nosync_4*) goto A; + end (* p___0 *) +(************************************************************) + + +(************************************************************) + automaton p___1 +(************************************************************) + actions: acts___2; + +loc A: invariant params___1 >= x___1 + when id = -1 do {x___1 := 0;} sync acts___2 goto req; + +loc req: invariant 2 >= x___1 + when 2 >= x___1 do {x___1 := 0; id := 1;} (* sync nosync_5*) goto waiting; + +loc waiting: invariant True + when id = -1 do {x___1 := 0;} (* sync nosync_6*) goto req; + when id = 1 +& x___1 > 2 do {} (* sync nosync_7*) goto cs; + +loc cs: invariant True + when True do {id := -1;} (* sync nosync_8*) goto A; + end (* p___1 *) +(************************************************************) + + +(************************************************************) +(* Initial state *) +(************************************************************) + +init := { + + discrete = + (*------------------------------------------------------------*) + (* Initial location *) + (*------------------------------------------------------------*) + loc[p___0] := A, + loc[p___1] := A, + (*------------------------------------------------------------*) + (* Initial discrete variables assignments *) + (*------------------------------------------------------------*) + id := -1 + ; + + (*------------------------------------------------------------*) + (* Initial continuous constraint *) + (*------------------------------------------------------------*) + continuous = + & params___0 >= 0 +& params___1 >= 0 +& x___0 = 0 +& x___1 = 1 + ; + +} + """ + }] + } + , ### THE END ] diff --git a/tests/testcases/templates/syntatic_check.imi b/tests/testcases/templates/syntatic_test.imi similarity index 88% rename from tests/testcases/templates/syntatic_check.imi rename to tests/testcases/templates/syntatic_test.imi index 80dee583..7897d4e9 100644 --- a/tests/testcases/templates/syntatic_check.imi +++ b/tests/testcases/templates/syntatic_test.imi @@ -28,7 +28,7 @@ loc cs: invariant True end -forall i in [0, 1]: instantiate p[i] := p(i); +forall i in [0, N - 1]: instantiate p[i] := p(i); init := { @@ -39,7 +39,7 @@ init := { continuous = forall i in [0, 1]: x[i] = i & - forall i in [0, 1]: params[i] >= 0 + forall i in [0, 2 * N - N - 1]: params[i] >= 0 ; }