Closed zhangyuanlin closed 6 years ago
This is a straightforward extension and I can work on it this weekend to expand the grammar and write the translation.
I believe this is fixed in the current calm.jar. Needs testing before I can close the issue.
Here is a test program I use. There is no syntax error. But in next comment, I'll show some problem.
system description test
theory test
module test
sort declarations
coordinates :: universe
points :: universe
attributes
x : 1..10
y : 1..10
locations :: universe
elevations :: universe
attributes
top: locations
constant declarations
p1 : points
x = 1
y = 9
topSth : locations
box: elevations
top = topSth % we allow term here
function declarations
statics
basic
number : 0..10
defined
intersect: booleans
axioms
function definitions
intersect if instance(X, 0..30), X = x(p1).
structure attribute_test
instances
b1, b2, b3 in locations
p(X, Y) in points
x = X
y = Y
e(X) in elevations
top = X
For program above (lets call it attribute.txt), the intermediate SPARC program has an error.
SPARC V2.54
temp.sp: non-ground term "p(X,Y)" occuring in program (line 190) as 1 argument of
predicate is_a/2 is not a program term.
Line 190 is
% Sort Instance [p(X, Y)] for sort [points].
is_a(p(X, Y), points) :- instance(X, range_pos_1_pos_10), instance(Y, range_pos_1_pos_10).
which should be from the ALM instantiation
p(X, Y) in points
x = X
y = Y
We need to think about how to address this. (SPARC may require any herbrand function symbol to be declared in a record sort, I need to double check.)
The intermediate SPARC program is
sorts
#comparable_integers_subsort = {}.
#range_pos_1_pos_10 = {}.
#range_pos_0_pos_30 = {}.
#range_pos_0_pos_10 = {}.
#integers = {}.
#singleton_topSth_locations___ = {}.
#locations = {topSth, b3, b2, b1}.
#coordinates = {}.
#singleton_p1_points___ = {}.
#points = {p1}.
#singleton_box_elevations___ = {}.
#elevations = {box, e(topSth), e(b3), e(b2), e(b1)}.
#actions = {}.
#universe = {b1, b2, b3, p1, topSth, box, e(b1), e(b2), e(b3), e(topSth)}.
#timeStep = {0, 1}.
#sort_hierarchy_nodes_ = {universe, timeStep, actions, booleans, integers, comparable_integers_subsort, coordinates, range_pos_1_pos_10, points, locations, elevations, singleton_p1_points___, singleton_topSth_locations___, singleton_box_elevations___, range_pos_0_pos_10, range_pos_0_pos_30}.
predicates
% Special Function [link]
link(#sort_hierarchy_nodes_, #sort_hierarchy_nodes_).
% Domain Function [dom_link].
dom_link(#sort_hierarchy_nodes_, #sort_hierarchy_nodes_).
% Attribute Function [top] for sort [elevations].
elevations_top(#elevations, #locations).
% Domain Function [dom_elevations_top] for attribute function [top] of sort [elevations].
dom_elevations_top(#elevations).
% Special Function [occurs]
occurs(#actions, #timeStep).
% Domain Function [dom_occurs].
dom_occurs(#actions, #timeStep).
% Special Function [subsort]
subsort(#sort_hierarchy_nodes_, #sort_hierarchy_nodes_).
% Domain Function [dom_subsort].
dom_subsort(#sort_hierarchy_nodes_, #sort_hierarchy_nodes_).
% Special Function [sink]
sink(#sort_hierarchy_nodes_).
% Domain Function [dom_sink].
dom_sink(#sort_hierarchy_nodes_).
% Static Function [number]
number(#range_pos_0_pos_10).
% Domain Function [dom_number].
dom_number().
% Special Function [has_parent]
has_parent(#sort_hierarchy_nodes_).
% Domain Function [dom_has_parent].
dom_has_parent(#sort_hierarchy_nodes_).
% Static Function [intersect]
intersect().
% Domain Function [dom_intersect].
dom_intersect().
% Special Function [instance]
instance(#universe, #sort_hierarchy_nodes_).
% Domain Function [dom_instance].
dom_instance(#universe, #sort_hierarchy_nodes_).
% Special Function [source]
source(#sort_hierarchy_nodes_).
% Domain Function [dom_source].
dom_source(#sort_hierarchy_nodes_).
% Special Function [has_child]
has_child(#sort_hierarchy_nodes_).
% Domain Function [dom_has_child].
dom_has_child(#sort_hierarchy_nodes_).
% Attribute Function [y] for sort [points].
points_y(#points, #range_pos_1_pos_10).
% Domain Function [dom_points_y] for attribute function [y] of sort [points].
dom_points_y(#points).
% Special Function [is_a]
is_a(#universe, #sort_hierarchy_nodes_).
% Domain Function [dom_is_a].
dom_is_a(#universe, #sort_hierarchy_nodes_).
% Attribute Function [x] for sort [points].
points_x(#points, #range_pos_1_pos_10).
% Domain Function [dom_points_x] for attribute function [x] of sort [points].
dom_points_x(#points).
rules
%---------------------
%-- Section: link
%---------------------
% [integers] is a child sort of [universe]
link(integers, universe).
% [range_pos_1_pos_10] is a child sort of [integers]
link(range_pos_1_pos_10, integers).
% [comparable_integers_subsort] is a child sort of [range_pos_1_pos_10]
link(comparable_integers_subsort, range_pos_1_pos_10).
% [range_pos_0_pos_30] is a child sort of [integers]
link(range_pos_0_pos_30, integers).
% [comparable_integers_subsort] is a child sort of [range_pos_0_pos_30]
link(comparable_integers_subsort, range_pos_0_pos_30).
% [range_pos_0_pos_10] is a child sort of [integers]
link(range_pos_0_pos_10, integers).
% [comparable_integers_subsort] is a child sort of [range_pos_0_pos_10]
link(comparable_integers_subsort, range_pos_0_pos_10).
% [locations] is a child sort of [universe]
link(locations, universe).
% [singleton_topSth_locations___] is a child sort of [locations]
link(singleton_topSth_locations___, locations).
% [coordinates] is a child sort of [universe]
link(coordinates, universe).
% [points] is a child sort of [universe]
link(points, universe).
% [singleton_p1_points___] is a child sort of [points]
link(singleton_p1_points___, points).
% [elevations] is a child sort of [universe]
link(elevations, universe).
% [singleton_box_elevations___] is a child sort of [elevations]
link(singleton_box_elevations___, elevations).
% [actions] is a child sort of [universe]
link(actions, universe).
%---------------------
%-- Section: is_a
%---------------------
% Sort Instance [b1] for sort [locations].
is_a(b1, locations).
% Sort Instance [b2] for sort [locations].
is_a(b2, locations).
% Sort Instance [b3] for sort [locations].
is_a(b3, locations).
% Sort Instance [p(X, Y)] for sort [points].
is_a(p(X, Y), points) :- instance(X, range_pos_1_pos_10), instance(Y, range_pos_1_pos_10).
% Sort Instance [e(X)] for sort [elevations].
is_a(e(X), elevations) :- instance(X, locations).
%---------------------
%-- Section: instance
%---------------------
% Base case of [instance] relation.
% If X is a Y then X is an instance of Y.
instance(X, Y) :- is_a(X, Y).
% Closure On [instance] relation.
% X is an instance of Z if X is an instance of Y and there is a link from Y to Z.
instance(X, Z) :- instance(X, Y), link(Y, Z).
%---------------------
%-- Section: subsort
%---------------------
% Base case of [subsort] relation.
% If there is a link from X to Y in the sort hierarchy then X is a subsort of Y.
subsort(X, Y) :- link(X, Y).
% Closure On [subsort] relation.
% X is a subsort of Z if there is a link from X to Y and Y is a subsort of Z.
subsort(X, Z) :- link(X, Y), subsort(Y, Z).
% [subsort] needs the closed world assumption since it is a total boolean function.
-subsort(X, Y) :- not subsort(X, Y).
%---------------------
%-- Section: has_parent
%---------------------
% Sort X has a parent in the hierarchy if there is a link from X to some sort Y.
has_parent(X) :- link(X, Y).
% [has_parent] needs the closed world assumption since it is a total boolean function.
-has_parent(X) :- not has_parent(X).
%---------------------
%-- Section: has_child
%---------------------
% X has a child in the hierarchy if there is a link from some sort Y to X.
has_child(X) :- link(Y, X).
% [has_child] needs the closed world assumption since it is a total boolean function.
-has_child(X) :- not has_child(X).
%---------------------
%-- Section: source
%---------------------
% If sort X has no child sort, X is a source sort
source(X) :- -has_child(X).
% [source] needs the closed world assumption since it is a total boolean function.
-source(X) :- not source(X).
%---------------------
%-- Section: sink
%---------------------
% If sort X has no parent sort, X is a sink sort
sink(X) :- -has_parent(X).
% [sink] needs the closed world assumption since it is a total boolean function.
-sink(X) :- not sink(X).
%---------------------
%-- Section: Auxiliary Rules For Static Functions
%---------------------
% Function [link] is a defined static function and has the closed world assumption.
-link(X0, X1) :- not link(X0, X1).
% Unique Assignment Constraint to model non-boolean functions using relations.
:- elevations_top(X0, V), elevations_top(X0, V2), V!=V2.
% Definition of [dom_elevations_top] when [elevations_top] is not a boolean function.
dom_elevations_top(X0) :- elevations_top(X0, V).
% Closed world assumption holds for [dom_elevations_top] since [elevations_top] is a static function.
-dom_elevations_top(X0) :- not dom_elevations_top(X0).
% Function [subsort] is a defined static function and has the closed world assumption.
-subsort(X0, X1) :- not subsort(X0, X1).
% Function [sink] is a defined static function and has the closed world assumption.
-sink(X0) :- not sink(X0).
% Unique Assignment Constraint to model non-boolean functions using relations.
:- number(V), number(V2), V!=V2.
% Definition of [dom_number] when [number] is not a boolean function.
dom_number :- number(V).
% Closed world assumption holds for [dom_number] since [number] is a static function.
-dom_number :- not dom_number.
% Function [has_parent] is a defined static function and has the closed world assumption.
-has_parent(X0) :- not has_parent(X0).
% Function [intersect] is a defined static function and has the closed world assumption.
-intersect :- not intersect.
% Function [instance] is a defined static function and has the closed world assumption.
-instance(X0, X1) :- not instance(X0, X1).
% Function [source] is a defined static function and has the closed world assumption.
-source(X0) :- not source(X0).
% Function [has_child] is a defined static function and has the closed world assumption.
-has_child(X0) :- not has_child(X0).
% Unique Assignment Constraint to model non-boolean functions using relations.
:- points_y(X0, V), points_y(X0, V2), V!=V2.
% Definition of [dom_points_y] when [points_y] is not a boolean function.
dom_points_y(X0) :- points_y(X0, V).
% Closed world assumption holds for [dom_points_y] since [points_y] is a static function.
-dom_points_y(X0) :- not dom_points_y(X0).
% Function [is_a] is a defined static function and has the closed world assumption.
-is_a(X0, X1) :- not is_a(X0, X1).
% Unique Assignment Constraint to model non-boolean functions using relations.
:- points_x(X0, V), points_x(X0, V2), V!=V2.
% Definition of [dom_points_x] when [points_x] is not a boolean function.
dom_points_x(X0) :- points_x(X0, V).
% Closed world assumption holds for [dom_points_x] since [points_x] is a static function.
-dom_points_x(X0) :- not dom_points_x(X0).
%---------------------
%-- Section: Axioms - State Constraints With Only Static Functions
%---------------------
% There are no rules in this section.
%---------------------
%-- Section: Axioms - Satic Function Definitions
%---------------------
% Definition for function [intersect].
intersect :- instance(X, range_pos_0_pos_30), #comparable_integers_subsort(X), points_x(p1, XO), X=XO.
%---------------------
%-- Section: Theory - Constant Declarations
%---------------------
% Constant [p1] declared for sort [points].
is_a(p1, points).
% Definition of attribute [x] for instance [p1] of sort [points].
points_x(p1, X_) :- instance(1, range_pos_1_pos_10), X_=1.
% Definition of attribute [y] for instance [p1] of sort [points].
points_y(p1, Y_) :- instance(9, range_pos_1_pos_10), Y_=9.
% Constant [topSth] declared for sort [locations].
is_a(topSth, locations).
% Constant [box] declared for sort [elevations].
is_a(box, elevations).
% Definition of attribute [top] for instance [box] of sort [elevations].
elevations_top(box, T_) :- instance(topSth, locations), T_=topSth.
%---------------------
%-- Section: Structure - Sort Instances
%---------------------
% Sort Instance [b1] for sort [locations].
is_a(b1, locations).
% Sort Instance [b2] for sort [locations].
is_a(b2, locations).
% Sort Instance [b3] for sort [locations].
is_a(b3, locations).
% Sort Instance [p(X, Y)] for sort [points].
is_a(p(X, Y), points) :- instance(X, range_pos_1_pos_10), instance(Y, range_pos_1_pos_10).
% Sort Instance [e(X)] for sort [elevations].
is_a(e(X), elevations) :- instance(X, locations).
%---------------------
%-- Section: Structure - Attribute Definitions
%---------------------
% Definition of attribute [x] for instance [p(X, Y)] of sort [points].
points_x(p(X, Y), X_) :- instance(X, range_pos_1_pos_10), #range_pos_1_pos_10(X), X_=X.
% Definition of attribute [y] for instance [p(X, Y)] of sort [points].
points_y(p(X, Y), Y_) :- instance(X, range_pos_1_pos_10), instance(Y, range_pos_1_pos_10), #range_pos_1_pos_10(Y), Y_=Y.
% Definition of attribute [top] for instance [e(X)] of sort [elevations].
elevations_top(e(X), T_) :- instance(X, locations), #locations(X), T_=X.
%---------------------
%-- Section: Structure - Static Function Definitions
%---------------------
% There are no rules in this section.
%---------------------
%-- Section: Axioms - Dynamic Causal Laws
%---------------------
% There are no rules in this section.
%---------------------
%-- Section: Axioms - Executability Conditions
%---------------------
% There are no rules in this section.
%---------------------
%-- Section: Axioms - State Constraints Containing Fluent Functions
%---------------------
% There are no rules in this section.
%---------------------
%-- Section: Axioms - Fluent Function Definitions
%---------------------
% There are no rules in this section.
% END OF PROGRAM
This issue is fixed in the code and will be available in the next release of the calm.jar.
Any sort could have attributes. Naturally, when we define a constant in a sort, we would like to define its attributes too. Example sort declarations