Maude-help mailing list

[Patrick Browne <patrick.browne AT dit.ie>]

Hi,
I am trying to approximate SEM specifications using Maude.
I am hoping to use the Maude search command enumerate the models.
The attached file contains the details. My questions are:

1) Can Maude approximate SEM model generation?
2) If Maude can provide some SEM functionality,
   how can I make my code provide that functionality?

Regards,
Pat Browne


This message has been scanned for content and viruses by the DIT Information 
Services E-Mail Scanning Service, and is believed to be clean. 
http://www.dit.ie***  
*** SEM[1] can generate models from specifications.
*** Given a set of axioms SEM can find their models.
*** I am trying to replicate some SEM specifications from [2] using Maude.
*** I am hoping to use the Maude search command will enumerate the models.
*** SEM produces all true and false cases from a model e.g.
*** in(Maine,Bangor) = $F
*** in(Maine,Maine) = $T
*** in(Maine,I95) = $F
*** in(Maine,river1) = $F
*** in(Orono,Maine) = $T
*** For the moment, I am interested in just the true cases.
*** Below is my attempt to encode the original SEM specification[2] in Maude.
*** I am focusing only on the IN predicate and some of its axioms.
*** The command search in(x,y) =>*  true does not produce any true results.
*** If the data equations are  reversed then the command search  true =>*  
in1(x,y) produces some true results.
*** My questions are:
***                 1) Can Maude approximate SEM model generation?
***                 2) If Maude can provide some SEM functionality, how can I 
make my code provide that functionality?
*** 
*** [1] Zhang, J. and Zhang, H. (1995). Sem: a system for enumerating models. 
*** http://dli.iiit.ac.in/ijcai/IJCAI-95-VOL%201/pdf/039.pdf
*** 
*** [2] Semantic Interoperability Of Geospatial Ontologies: A Model-Theoretic 
Analysis, James A. Farrugia, PhD thesis 2007
*** http://www.library.umaine.edu/theses/pdf/FarrugiaJA2007.pdf
*** 

mod MODELCHECK is
sort Thing .
op Route2 : -> Thing .
op Orono : -> Thing .
op Bangor : -> Thing .
op Maine : -> Thing .
op I95 : -> Thing .
op river1 : -> Thing .
***  Functions
op state : Thing -> Bool .
op town : Thing -> Bool .
op road : Thing -> Bool .
op river : Thing -> Bool .
op in : Thing Thing -> Bool .
op through : Thing Thing -> Bool .


vars x y z : Thing .

*** IN is reflexive, antisymmetric, and transitive
eq   [IN1] : in(x,x) = true .
ceq  [IN2] : (x == y) = true if in(y,x)  and in(x,y) [nonexec]  .
ceq  [IN3] : in(x,z) = true if (in(x,y) and in(y,z)) [nonexec]  .  


*** towns, roads, rivers, and states are all pairwise disjoint
eq town(x) and road(x)   = false .
eq town(x) and  river(x)   = false .
eq town(x) and  state(x)   = false .
eq road(x) and  river(x)   = false .
eq road(x) and  state(x)   = false  .
eq river(x) and  state(x)   = false  .

*** if x and y are different roads/rivers/towns/states, then x can’t be IN y
*** don't think I need to check both in(x,y) and in(y,x)
ceq  in(x,y)   = false if road(x) and road(y) and  not(x == y) .
ceq  in(x,y)   = false if river(x) and river(y) and  not(x == y) .
ceq  in(x,y)   = false if town(x) and town(y) and  not(x == y) .
ceq  in(x,y)   = false if state(x) and state(y) and  not(x == y) .

*** if x is a state and y is a town,  then x is NOT IN y
ceq [townState] : in(x,y) = false if (state(x) and town(y))  .


*** data: does not seem to work when ..=> true
*** the command search, in1(x,y) =>*  true, gives not true results
*** rl town(Orono)  => true .
*** rl town(Bangor)  => true .
*** rl road(Route2)  => true .
*** rl road(I95)   => true .
*** rl state(Maine)  => true .
*** rl river(river1)  => true .
*** rl in(Orono, Maine)  => true .
*** rl in(Bangor, Maine)  => true .

*** data : I get some results when true => ..
rl true =>  town(Orono)   .
rl true =>  town(Bangor)  .
rl true =>  road(Route2)  .
rl true => road(I95) .
rl true =>  state(Maine)   .
rl true =>  river(river1)   .
rl true =>  in(Orono, Maine)  .

endm

eof

search  true =>*  in1(x,y) .
gives some results
 
 
%% Original SEM specification file ch5O2.in.
%% Sorts
( thing : Route2, Orono, Bangor, Maine, I95, river1 )
%% Functions
{ state : thing -> BOOL }
{ town : thing -> BOOL }
{ road : thing -> BOOL }
{ river : thing -> BOOL }
{ in : thing thing -> BOOL }
{ through : thing thing -> BOOL }
%% Clauses (Axioms)
% IN is reflexive, antisymmetric, and transitive
[ in(x,x) ]
[ x=y | -in(x,y) | -in(y,x) ]
[ -in(x,y) | -in(y,z) | in(x,z)]
% THROUGH is antisymmetric and transitive
[ x=y | -through(x,y) | -through(y,x) ]
[ -through(x,y) | -through(y,z) | through(x,z)]

% towns, roads, rivers, and states are
% all pairwise disjoint
[ -town(x) | -road(x) ]
[ -town(x) | -river(x) ]
[ -town(x) | -state(x) ]
[ -road(x) | -river(x) ]
[ -road(x) | -state(x) ]
[ -river(x) | -state(x) ]

% if x and y are different roads/rivers/towns/states,
% then x is NOT IN y
[ x=y | -road(x) | -road(y) | -in(x,y) ]
[ x=y | -road(x) | -road(y) | -in(y,x) ]
[ x=y | -river(x) | -river(y) | -in(x,y) ]
[ x=y | -river(x) | -river(y) | -in(y,x) ]
[ x=y | -town(x) | -town(y) | -in(x,y) ]
[ x=y | -town(x) | -town(y) | -in(y,x) ]
[ x=y | -state(x) | -state(y) | -in(x,y) ]
[ x=y | -state(x) | -state(y) | -in(y,x) ]

% if x is a town/state/river and y is a road,
% then x is NOT IN y
[ -town(x) | -road(y) | -in(x,y) ]
[ -state(x) | -road(y) | -in(x,y) ]
[ -river(x) | -road(y) | -in(x,y) ]

% if x is a road/town/state and y is a river,
% then x is NOT IN y
[ -road(x) | -river(y) | -in(x,y) ]
[ -town(x) | -river(y) | -in(x,y) ]
[ -state(x) | -river(y) | -in(x,y) ]

% if x is a state and y is a town,
% then x is NOT IN y
[ -state(x) | -town(y) | -in(x,y) ]

% if x is a state and y is a town,
% then x does NOT go THROUGH y
[ -state(x) | -town(y) | -through(x,y) ]

% if x is a town/state and y is a road,
% then x does NOT go THROUGH y
[ -town(x) | -road(y) | -through(x,y) ]
[ -state(x) | -road(y) | -through(x,y) ]

% if x is a town/state/road and y is a river,
% then x does NOT go THROUGH y
[ -town(x) | -river(y) | -through(x,y) ]
[ -state(x) | -river(y) | -through(x,y) ]
[ -road(x) | -river(y) | -through(x,y) ]

% if x is a town/state and y is a town,
% then x does NOT go THROUGH y
[ -town(x) | -town(y) | -through(x,y) ]
[ -state(x) | -town(y) | -through(x,y) ]
% if x goes THROUGH y, then y is NOT IN x
[ -through(x,y) | -in(y,x) ]


% data
[ town(Orono) ]
[ town(Bangor) ]
[ road(Route2) ]
[ road(I95) ]
[ state(Maine) ]
[ river(river1) ]
[ in(Orono, Maine) ]
[ in(Bangor, Maine) ]
[ through(river1, Bangor) ]
[ through(river1, Orono) ]
[ through(river1, Maine) ]
[ through(I95, Bangor) ]
[ through(I95, Orono) ]
[ through(I95, Maine) ]
[ through(Route2, Bangor) ]
[ through(Route2, Orono) ]
[ through(Route2, Maine) ]
[ -through(Orono, Maine) ]
[ -through(Bangor, Maine) ]
%  There are 1250 models of ch5O2.in.