Skip to content
Snippets Groups Projects
Commit 6940f75e authored by Dennis Hendriks's avatar Dennis Hendriks
Browse files

#1110 Add more CIF explorer tests.

parent aab0a453
No related branches found
No related tags found
2 merge requests!1242#1072 develop to master for v7.0-M1,!1198#1110 CIF explorer gets various improvements/fixes relating to 'not too many initial states' precondition
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2025 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////
automaton a:
disc int x in any;
invariant x >= 0;
location:
initial;
end
automaton b:
disc bool x in any;
location:
initial x != x;
end
ERROR: CIF explorer failed due to unsatisfied preconditions:
------------------------------------------------------------------------------------------------------------------------
(1/1) The specification has approximately 8.589934592e9 possible initial states, more than the maximum of 2,147,483,647.
------------------------------------------------------------------------------------------------------------------------
automaton statespace:
alphabet;
location;
end
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2025 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////
automaton a:
disc int x in any;
invariant x >= 0;
location:
initial;
end
automaton b:
location:
initial false;
end
No initial state found.
WARNING: File "explorer/no_initial_var_many_aut_none.cif": Semantic warning at line 21, column 11: Automaton "b" has no initial location.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment