This is Appendix C of the Semantic Web Services Ontology (SWSO) document.
Here we give the Rules Ontology for Web Services (ROWS) formulations of the axioms of the process model, as described in Section 3 of the SWSO document. ROWS is also known as SWSO-Rules. These formulations are derived directly from the FLOWS (SWSO-FOL) formulations, as given in Appendix B, according to the translation approach described in Section 3 of the SWSL document. They can easily be compared to the FLOWS axioms by viewing Appendices B and C in two browser windows side by side.
The hyperlinked concept and relation names refer to concepts and relations defined in the Process Specification Language (PSL).
Every service is associated with an activity.
service_activity(?s, _#(?s)) :- service(?s). neg service(?s) :- neg service_activity(?s, _#(?s)). Note: The two rules above are the omnidirectional set of rules for this (skolemized) clause: neg service(?s) or service_activity(?s, _#(?s)). which is equivalent to this: service(?s) ==> service_activity(?s, _#(?s)).
A service activity is an activity in the PSL Ontology.
activity(?a) :- service_activity(?s,?a). neg service_activity(?s,?a) :- neg activity(?a).
A service occurrence is an occurrence of the activity that is associated with the service.
neg service_occurrence(?s,?o) :- occurrence_of(?o,?a) and neg service_activity(?s,?a). neg occurrence_of(?o,?a) :- service_occurrence(?s,?o) and neg service_activity(?s,?a). service_activity(?s,?a) :- service_occurrence(?s,?o) and occurrence_of(?o,?a). Note: The three rules above are the omnidirectional set of rules for this clause: neg service_occurrence(?s,?o) or neg occurrence_of(?o,?a) or service_activity(?s,?a). which is equivalent to this: service_occurrence(?s,?o) and occurrence_of(?o,?a) ==> service_activity(?s,?a).
An AtomicProcess is equivalent to a primitive activity in the PSL Ontology such that its preconditions and effects depend only on the fluents that hold prior to the an occurrence of the activity.
AtomicProcess(?a) :- primitive(?a) and markov_precond(?a) and markov_effects(?a). neg primitive(?a) :- neg AtomicProcess(?a) and markov_precond(?a) and markov_effects(?a). neg markov_precond(?a) :- neg AtomicProcess(?a) and primitive(?a) and markov_effects(?a). neg markov_effects(?a) :- neg AtomicProcess(?a) and primitive(?a) and markov_precond(?a). AtomicProcess(?a) :- primitive(?a) and markov_precond(?a) and context_free(?a). neg primitive(?a) :- neg AtomicProcess(?a) and markov_precond(?a) and context_free(?a). neg markov_precond(?a) :- neg AtomicProcess(?a) and primitive(?a) and context_free(?a). neg context_free(?a) :- neg AtomicProcess(?a) and primitive(?a) and markov_precond(?a). primitive(?a) :- AtomicProcess(?a). neg AtomicProcess(?a) :- neg primitive(?a). markov_precond(?a) :- AtomicProcess(?a). neg AtomicProcess(?a) :- neg markov_precond(?a). neg AtomicProcess(?a) :- neg markov_effects(?a) and neg context_free(?a). markov_effects(?a) :- neg context_free(?a) and AtomicProcess(?a). context_free(?a) :- AtomicProcess(?a) and neg markov_effects(?a). Note: The first 8 rules above are the omnidirectional sets of rules for these two disjunctions: AtomicProcess(?a) or not primitive(?a) or not markov_precond(?a) or neg markov_effects(?a). AtomicProcess(?a) or not primitive(?a) or not markov_precond(?a) or neg context_free(?a). which (conjoined) are equivalent to the impliedBy (<==) direction of the SWSO-FOL axiom: forall ?a (AtomicProcess(?a) <== (primitive(?a) and markov_precond(?a) and (markov_effects(?a) or context_free(?a))). The last 7 rules above are the omnidirectional sets for these clauses: neg AtomicProcess(?a) or primitive(?a) neg AtomicProcess(?a) or markov_precond(?a) neg AtomicProcess(?a) or markov_effects(?a) or context_free(?a) which together are equivalent to the implies (==>) direction of the SWSO-FOL axiom.
If a fluent is an input to an activity, then the reference of the fluent must be known as a precondition for the activity to occur.
prior(Kref(?iofluent),?s)) :- occurrence_of(?s,?a) and legal(?s) and input(?a,?iofluent). neg occurrence_of(?s,?a) :- neg prior(Kref(?iofluent),?s)) and legal(?s) and input(?a,?iofluent). neg legal(?s) :- neg prior(Kref(?iofluent),?s)) and occurrence_of(?s,?a) and input(?a,?iofluent). neg input(?a,?iofluent) :- neg prior(Kref(?iofluent),?s)) and occurrence_of(?s,?a) and legal(?s).
If ?iofluent is an output to an activity that is conditional on the fluent ?f, then the effect of the activity occurrence when ?f holds prior to the activity occurrence is that the reference of ?iofluent is known.
holds(Kref(?iofluent),?s)) :- occurrence_of(?s,?a) and legal(?s) and prior(?f,s) and output(?a,?iofluent,?f). neg occurrence_of(?s,?a) :- neg holds(Kref(?iofluent),?s)) and legal(?s) and prior(?f,s) output(?a,?iofluent,?f). neg legal(?s) :- neg holds(Kref(?iofluent),?s)) and occurrence_of(?s,?a) and prior(?f,s) and output(?a,?iofluent,?f). neg prior(?f,s) :- neg holds(Kref(?iofluent),?s)) and occurrence_of(?s,?a) and legal(?s) and output(?a,?iofluent,?f). neg output(?a,?iofluent,?f) :- neg holds(Kref(?iofluent),?s)) and occurrence_of(?s,?a) and legal(?s) and prior(?f,s).
The following axioms define the epistemic fluents.
The K fluent represents the accessibility relation in the possible-world model of knowledge. An activity occurrence ?s1 is accessible from an activity occurrence ?s if as far as is known in ?s, ?s1 might have occurred.
neg occurrence_of(?s,?a) :- holds(K(?s2),?s) and ?s2 :=: successor(?a,_#1(?a,?s,?s2)). neg holds(K(?s2),?s) :- occurrence_of(?s,?a) and neg ?s2 :=: successor(?a,_#1(?a,?s,?s2)). ?s2 :=: successor(?a,_#1(?a,?s,?s2)) :- occurrence_of(?s,?a) and holds(K(?s2),?s). neg occurrence_of(?s,?a) :- holds(K(?s2),?s) and neg legal(?s2). neg holds(K(?s2),?s) :- occurrence_of(?s,?a) and neg legal(?s2). legal(?s2) :- occurrence_of(?s,?a) and holds(K(?s2),?s). neg occurrence_of(?s,?a) :- holds(K(?s2),?s) and neg holds(K(_#1(?a,?s,?s2)),?s). neg holds(K(?s2),?s) :- occurrence_of(?s,?a) and neg holds(K(_#1(?a,?s,?s2)),?s). holds(K(_#1(?a,?s,?s2)),?s) :- occurrence_of(?s,?a) and holds(K(?s2),?s). neg occurrence_of(?s,?a) :- holds(K(?s2),?s) and neg SR(?a,?s) :=: SR(?a,_#1(?a,?s,?s2)). neg holds(K(?s2),?s) :- occurrence_of(?s,?a) and neg SR(?a,?s) :=: SR(?a,_#1(?a,?s,?s2)). SR(?a,?s) :=: SR(?a,_#1(?a,?s,?s2)) :- occurrence_of(?s,?a) and holds(K(?s2),?s). neg occurrence_of(?s,?a) :- neg holds(K(?s2),?s) and (?s2 :=: successor(?a,?s1) and legal(?s2) and holds(K(?s1),?s) and (SR(?a,?s) :=: SR(?a,?s1)). neg holds(K(?s2),?s) :- occurrence_of(?s,?a) and (?s2 :=: successor(?a,?s1) and legal(?s2) and holds(K(?s1),?s) and (SR(?a,?s) :=: SR(?a,?s1)). neg (?s2 :=: successor(?a,?s1) :- occurrence_of(?s,?a) and neg holds(K(?s2),?s) and legal(?s2) and holds(K(?s1),?s) and (SR(?a,?s) :=: SR(?a,?s1)). neg legal(?s2) :- occurrence_of(?s,?a) and neg holds(K(?s2),?s) and (?s2 :=: successor(?a,?s1) and holds(K(?s1),?s) and (SR(?a,?s) :=: SR(?a,?s1)). neg holds(K(?s1),?s) :- occurrence_of(?s,?a) and neg holds(K(?s2),?s) and (?s2 :=: successor(?a,?s1) and legal(?s2) and (SR(?a,?s) :=: SR(?a,?s1)). neg (SR(?a,?s) :=: SR(?a,?s1)) :- occurrence_of(?s,?a) and neg holds(K(?s2),?s) and (?s2 :=: successor(?a,?s1) and legal(?s2) and holds(K(?s1),?s).
The Knows fluent holds if the K fluent holds at all accessible activity occurrences.
neg holds(Knows(?f),?s) :- holds(K(?sp),?s) and neg holds(?f,?sp). neg holds(K(?sp),?s) :- holds(Knows(?f),?s) and neg holds(?f,?sp). holds(?f,?sp) :- holds(Knows(?f),?s) and holds(K(?sp),?s). holds(Knows(?f),?s) :- neg holds(K(_#1(?f,?s)),?s) and holds(?f,_#1(?f,?s)). holds(K(_#1(?f,?s)),?s) :- neg holds(Knows(?f),?s) and holds(?f,_#1(?f,?s)). neg holds(?f,_#1(?f,?s)) :- neg holds(Knows(?f),?s) and neg holds(K(_#1(?f,?s)),?s).
The fluent neg is used to reify negation for fluent terms.
holds(neg(?f), ?s) :- neg holds(?f, ?s). holds(?f, ?s) :- neg holds(neg(?f), ?s). neg holds(?f, ?s) :- holds(neg(?f), ?s). neg holds(neg(?f), ?s) :- holds(?f, ?s).
The Kref fluent holds whenever the reference of its argument is known.
holds(Kref(?f), ?s) :- holds(Knows(?f :=: ?x), ?s). neg (holds(Knows(?f :=: ?x),?s)) :- neg holds(Kref(?f),?s). holds(Knows(?f :=: _#(?f,?s)), ?s) :- holds(Kref(?f), ?s). neg holds(Kref(?f), ?s) :- neg holds(Knows(?f :=: _#(?f,?s)), ?s).
The composedOf relation is equivalent to the subactivity relation in the PSL Ontology.
composedOf(?a1,?a2) :- subactivity(?a2,?a1). neg subactivity(?a2,?a1) :- neg composedOf(?a1,?a2). subactivity(?a2,?a1) :- composedOf(?a1,?a2). neg composedOf(?a1,?a2) :- neg subactivity(?a2,?a1).
A Split activity is equivalent to a strong_poset activity in PSL. The activity trees all have the same structure and each activity tree consists of branches that are in one-to-one correspondence with sequences of subactivity occurrences that satisfy the partial ordering constraints.
Split(?a) :- uniform(?a) and occurrence_of(?occ,?a) and neg simple(?occ) and ordered(?occ) and strong_poset(?occ). neg uniform(?a) :- neg Split(?a) and occurrence_of(?occ,?a) and neg simple(?occ) and ordered(?occ) and strong_poset(?occ). neg occurrence_of(?occ,?a) :- neg Split(?a) and uniform(?a) and neg simple(?occ) and ordered(?occ) and strong_poset(?occ). simple(?occ) :- neg Split(?a) and uniform(?a) and occurrence_of(?occ,?a) and ordered(?occ) and strong_poset(?occ). neg ordered(?occ) :- neg Split(?a) and uniform(?a) and occurrence_of(?occ,?a) and neg simple(?occ) and strong_poset(?occ). neg strong_poset(?occ) :- neg Split(?a) and uniform(?a) and occurrence_of(?occ,?a) and neg simple(?occ) and ordered(?occ). uniform(?a) and occurrence_of(_#1(?a),?a) and neg simple(_#1(?a)) and ordered(_#1(?a)) and strong_poset(_#1(?a)) :- Split(?a). neg Split(?a) :- neg uniform(?a). neg Split(?a) :- neg occurrence_of(_#1(?a),?a). neg Split(?a) :- simple(_#1(?a)). neg Split(?a) :- neg ordered(_#1(?a)). neg Split(?a) :- neg strong_poset(_#1(?a)).
A Sequence activity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree consists of a unique branch.
Sequence(?a) :- uniform(?a) and occurrence_of(?occ,?a) and simple(?occ) and rigid(?occ) and ordered(?occ) and strong_poset(?occ). neg uniform(?a) :- neg Sequence(?a) and occurrence_of(?occ,?a) and simple(?occ) and rigid(?occ) and ordered(?occ) and strong_poset(?occ). neg occurrence_of(?occ,?a) :- neg Sequence(?a) and uniform(?a) and simple(?occ) and rigid(?occ) and ordered(?occ) and strong_poset(?occ). neg simple(?occ) :- neg Sequence(?a) and uniform(?a) and occurrence_of(?occ,?a) and rigid(?occ) and ordered(?occ) and strong_poset(?occ). neg rigid(?occ) :- neg Sequence(?a) and uniform(?a) and occurrence_of(?occ,?a) and simple(?occ) and ordered(?occ) and strong_poset(?occ). neg ordered(?occ) :- neg Sequence(?a) and uniform(?a) and occurrence_of(?occ,?a) and simple(?occ) and rigid(?occ) and strong_poset(?occ). neg strong_poset(?occ) :- neg Sequence(?a) and uniform(?a) and occurrence_of(?occ,?a) and simple(?occ) and rigid(?occ) and ordered(?occ). uniform(?a) and occurrence_of(_#1(?a),?a) and simple(_#1(?a)) and rigid(_#1(?a)) and ordered(_#1(?a)) and strong_poset(_#1(?a)) :- Sequence(?a). neg Sequence(?a) :- neg uniform(?a). neg Sequence(?a) :- neg occurrence_of(_#1(?a),?a). neg Sequence(?a) :- neg simple(_#1(?a)). neg Sequence(?a) :- neg rigid(_#1(?a)). neg Sequence(?a) :- neg ordered(_#1(?a)). neg Sequence(?a) :- neg strong_poset(_#1(?a)).
An Unordered activity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree is a bag. In this case, there is a one-to-one correspondence between branches of the activity tree and all permutations of subactivity occurrences.
Unordered(?a) :- uniform(?a) and occurrence_of(?occ,?a) and bag(?occ). neg uniform(?a) :- Unordered(?a) and occurrence_of(?occ,?a) and bag(?occ). neg occurrence_of(?occ,?a) :- neg Unordered(?a) and uniform(?a) and bag(?occ). neg bag(?occ) :- neg Unordered(?a) and uniform(?a) and occurrence_of(?occ,?a). uniform(?a) and occurrence_of(_#1(?a),?a) and bag(_#1(?a)) :- Unordered(?a). neg Unordered(?a) :- neg uniform(?a). neg Unordered(?a) :- neg occurrence_of(_#1(?a),?a). neg Unordered(?a) :- neg bag(_#1(?a)).
A Choice activity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree is nondeterministic (that is, each branch contains occurrences of different subactivities.
Choice(?a) :- uniform(?a) and occurrence_of(?occ,?a) and simple(?occ) and rigid(?occ) and unordered(?occ) and choice_poset(?occ). neg uniform(?a) :- neg Choice(?a) and occurrence_of(?occ,?a) and simple(?occ) and rigid(?occ) and unordered(?occ) and choice_poset(?occ). neg occurrence_of(?occ,?a) :- neg Choice(?a) and uniform(?a) and simple(?occ) and rigid(?occ) and unordered(?occ) and choice_poset(?occ). neg simple(?occ) :- neg Choice(?a) and uniform(?a) and occurrence_of(?occ,?a) and rigid(?occ) and unordered(?occ) and choice_poset(?occ). neg rigid(?occ) :- neg Choice(?a) and uniform(?a) and occurrence_of(?occ,?a) and simple(?occ) and unordered(?occ) and choice_poset(?occ). neg unordered(?occ) :- neg Choice(?a) and uniform(?a) and occurrence_of(?occ,?a) and simple(?occ) and rigid(?occ) and choice_poset(?occ). neg choice_poset(?occ) :- neg Choice(?a) and uniform(?a) and occurrence_of(?occ,?a) and simple(?occ) and rigid(?occ) and unordered(?occ). uniform(?a) and occurrence_of(_#1(?a),?a) and neg simple(_#1(?a)) and rigid(_#1(?a)) and unordered(_#1(?a)) and choice_poset(_#1(?a)) :- Choice(?a). neg Choice(?a) :- neg uniform(?a). neg Choice(?a) :- neg occurrence_of(_#1(?a),?a). neg Choice(?a) :- simple(_#1(?a)). neg Choice(?a) :- neg rigid(_#1(?a)). neg Choice(?a) :- neg unordered(_#1(?a)). neg Choice(?a) :- neg choice_poset(_#1(?a)).
An IfThenElse activity is equivalent to a conditional activity in the PSL Ontology.
IfThenElse(?a) :- conditional(?a). neg conditional(?a) :- neg IfThenElse(?a). conditional(?a) :- IfThenElse(?a). neg IfThenElse(?a) :- neg conditional(?a).
An Iterate activity is equivalent to an activity in the PSL Ontology whose occurrences are repetitive. Activity trees for this activity have different structure, depending on the cardinality of the repeated subtrees.
Iterate(?a) :- activity(?a) and neg occurrence_of(_#1(?a),?a). neg activity(?a) :- neg Iterate(?a) and neg occurrence_of(_#1(?a),?a). occurrence_of(_#1(?a),?a) :- neg Iterate(?a) and activity(?a). Iterate(?a) :- activity(?a) and repetitive(_#1(?a)) and multiple_outcome(_#1(?a)). neg activity(?a) :- neg Iterate(?a) and repetitive(_#1(?a)) and multiple_outcome(_#1(?a)). neg repetitive(_#1(?a)) :- neg Iterate(?a) and activity(?a) and multiple_outcome(_#1(?a)). neg multiple_outcome(_#1(?a)) :- neg Iterate(?a) and activity(?a) and repetitive(_#1(?a)). neg Iterate(?a) :- neg activity(?a). activity(?a) :- Iterate(?a). neg Iterate(?a) :- occurrence_of(?occ,?a) and neg repetitive(?occ). neg occurrence_of(?occ,?a) :- Iterate(?a) and neg repetitive(?occ). repetitive(?occ) :- Iterate(?a) and occurrence_of(?occ,?a). neg Iterate(?a) :- occurrence_of(?occ,?a) and neg multiple_outcome(?occ). neg occurrence_of(?occ,?a) :- Iterate(?a) and neg multiple_outcome(?occ). multiple_outcome(?occ) :- Iterate(?a) and occurrence_of(?occ,?a).
A RepeatUntil activity is equivalent to a conditional activity in the PSL Ontology whose occurrences are repetitive. Activity trees for this activity have different structure, depending on the cardinality of the repeated subtrees.
RepeatUntil(?a) :- conditional(?a) and neg occurrence_of(_#1(?a),?a). neg conditional(?a) :- neg RepeatUntil(?a) and neg occurrence_of(_#1(?a),?a). occurrence_of(_#1(?a),?a) :- neg RepeatUntil(?a) and conditional(?a). RepeatUntil(?a) :- conditional(?a) and repetitive(_#1(?a)) and multiple_outcome(_#1(?a). neg conditional(?a) :- neg RepeatUntil(?a) and repetitive(_#1(?a)) and multiple_outcome(_#1(?a)). neg repetitive(_#1(?a)) :- neg RepeatUntil(?a) and conditional(?a) and multiple_outcome(_#1(?a)). neg multiple_outcome(_#1(?a)) :- neg RepeatUntil(?a) and conditional(?a) and repetitive(_#1(?a)). neg RepeatUntil(?a) :- neg activity(?a). activity(?a) :- RepeatUntil(?a). neg RepeatUntil(?a) :- neg conditional(?a). conditional(?a) :- RepeatUntil(?a). neg RepeatUntil(?a) :- occurrence_of(?occ,?a) and neg repetitive(?occ). neg occurrence_of(?occ,?a) :- RepeatUntil(?a) and neg repetitive(?occ). repetitive(?occ) :- RepeatUntil(?a) and occurrence_of(?occ,?a). neg RepeatUntil(?a) :- occurrence_of(?occ,?a) and neg multiple_outcome(?occ). neg occurrence_of(?occ,?a) :- RepeatUntil(?a) and neg multiple_outcome(?occ). multiple_outcome(?occ) :- RepeatUntil(?a) and occurrence_of(?occ,?a).
An Ordered activity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree is ordered if and only if the branches contain occurrences of the same subactivities.
OrderedActivity(?a) :- uniform(?a) and occurrence_of(?occ,?a) and neg simple(?occ) and ordered(?occ). neg uniform(?a) :- neg OrderedActivity(?a) and occurrence_of(?occ,?a) and neg simple(?occ) and ordered(?occ). neg occurrence_of(?occ,?a) :- neg OrderedActivity(?a) and uniform(?a) and neg simple(?occ) and ordered(?occ). simple(?occ) :- neg OrderedActivity(?a) and uniform(?a) and occurrence_of(?occ,?a) and ordered(?occ). neg ordered(?occ) :- neg OrderedActivity(?a) and uniform(?a) and occurrence_of(?occ,?a) and neg simple(?occ). OrderedActivity(?a) :- uniform(?a) and occurrence_of(?occ,?a) and simple(?occ) and neg ordered(?occ). neg uniform(?a) :- neg OrderedActivity(?a) and occurrence_of(?occ,?a) and simple(?occ) and neg ordered(?occ). neg occurrence_of(?occ,?a) :- neg OrderedActivity(?a) and uniform(?a) and simple(?occ) and neg ordered(?occ). neg simple(?occ) :- neg OrderedActivity(?a) and uniform(?a) and occurrence_of(?occ,?a) and neg ordered(?occ). ordered(?occ) :- neg OrderedActivity(?a) and uniform(?a) and occurrence_of(?occ,?a) and simple(?occ). neg OrderedActivity(?a) :- neg uniform(?a). uniform(?a) :- OrderedActivity(?a). neg OrderedActivity(?a) :- neg occurrence_of(_#1(?a),?a). occurrence_of(_#1(?a),?a) :- OrderedActivity(?a). neg OrderedActivity(?a) :- neg ordered(_#1(?a)) and neg simple(_#1(?a)). ordered(_#1(?a)) :- OrderedActivity(?a) and neg simple(_#1(?a)). simple(_#1(?a)) :- OrderedActivity(?a) and neg ordered(_#1(?a)). neg OrderedActivity(?a) :- ordered(_#1(?a)) and simple(_#1(?a)). neg ordered(_#1(?a)) :- OrderedActivity(?a) and simple(_#1(?a)). neg simple(_#1(?a)) :- OrderedActivity(?a) and ordered(_#1(?a)).
An Ordered activity is equivalent to an activity in PSL whose activity trees all have the same structure and such that each activity tree is ordered if and only if the branches contain occurrences of the same subactivities.
OccActivity(?a) :- uniform(?a) and occurrence_of(?occ,?a) and permuted(?occ). neg uniform(?a) :- neg OccActivity(?a) and occurrence_of(?occ,?a) and permuted(?occ). neg occurrence_of(?occ,?a) :- neg OccActivity(?a) and uniform(?a) and permuted(?occ). neg permuted(?occ) :- neg OccActivity(?a) and uniform(?a) and occurrence_of(?occ,?a). OccActivity(?a) :- uniform(?a) and occurrence_of(?occ,?a) and neg nondet_permuted(?occ). neg uniform(?a) :- neg OccActivity(?a) and occurrence_of(?occ,?a) and neg nondet_permuted(?occ). neg occurrence_of(?occ,?a) :- neg OccActivity(?a) and uniform(?a) and neg nondet_permuted(?occ). nondet_permuted(?occ) :- neg OccActivity(?a) and uniform(?a) and occurrence_of(?occ,?a). neg OccActivity(?a) :- neg uniform(?a). uniform(?a) :- OccActivity(?a). neg OccActivity(?a) :- neg occurrence_of(_#1(?a),?a). occurrence_of(_#1(?a),?a) :- OccActivity(?a). neg OccActivity(?a) :- neg permuted(_#1(?a)) and neg nondet_permuted(_#1(?a)). permuted(_#1(?a)) :- OccActivity(?a) and neg nondet_permuted(_#1(?a)). nondet_permuted(_#1(?a)) :- OccActivity(?a) and neg permuted(_#1(?a)).
A TriggeredActivity is equivalent to a trigger activity in the PSL Ontology.
TriggeredActivity(?a) :- trigger(?a). neg trigger(?a) :- neg TriggeredActivity(?a). trigger(?a) :- TriggeredActivity(?a). neg TriggeredActivity(?a) :- neg trigger(?a).
Messages are objects in the ontology.
object(?m) :- message_info(?m,?msgtype,?x). neg message_info(?m,?msgtype,?x) :- neg object(?m).
A message is produced, read, or destroyed by an AtomicProcess.
neg produces(?o,?m) :- occurrence_of(?o,?a) and neg AtomicProcess(?a). neg occurrence_of(?o,?a) :- produces(?o,?m) and neg AtomicProcess(?a). AtomicProcess(?a) :- produces(?o,?m) and occurrence_of(?o,?a). neg reads(?o,?m) :- occurrence_of(?o,?a) and neg AtomicProcess(?a). neg occurrence_of(?o,?a) :- reads(?o,?m) and neg AtomicProcess(?a). AtomicProcess(?a) :- reads(?o,?m) and occurrence_of(?o,?a). neg destroys(?o,?m) :- occurrence_of(?o,?a) and neg AtomicProcess(?a). neg occurrence_of(?o,?a) :- destroys(?o,?m) and neg AtomicProcess(?a). AtomicProcess(?a) :- destroys(?o,?m) and occurrence_of(?o,?a).
For any occurrence that reads a message, the reference of the input described by the message type is known after the occurrence.
holds(Kref(?iofluent),?o)) :- reads(?o,?m) and message_info(?m,?msgtype,?x) and described_by(?msgtype,?iofluent) and legal(?o). neg reads(?o,?m) :- message_info(?m,?msgtype,?x) and described_by(?msgtype,?iofluent) and legal(?o) and neg holds(Kref(?iofluent),?o)). neg message_info(?m,?msgtype,?x) :- reads(?o,?m) and described_by(?msgtype,?iofluent) and legal(?o) and neg holds(Kref(?iofluent),?o)). neg described_by(?msgtype,?iofluent) :- reads(?o,?m) and message_info(?m,?msgtype,?x) and legal(?o) and neg holds(Kref(?iofluent),?o)). neg legal(?o) :- reads(?o,?m) and message_info(?m,?msgtype,?x) and described_by(?msgtype,?iofluent) and neg holds(Kref(?iofluent),?o)).
For any occurrence that produces a message, the reference of the output described by the message is known before the occurrence.
prior(Kref(?iofluent),?o)) :- produces(?o,?m) and message_info(?m,?msgtype,?x) and described_by(?msgtype,?iofluent) and legal(?o). neg produces(?o,?m) :- message_info(?m,?msgtype,?x) and described_by(?msgtype,?iofluent) and legal(?o) and neg prior(Kref(?iofluent),?o)). neg message_info(?m,?msgtype,?x) :- produces(?o,?m) and described_by(?msgtype,?iofluent) and legal(?o) and neg prior(Kref(?iofluent),?o)). neg described_by(?msgtype,?iofluent) :- produces(?o,?m) and message_info(?m,?msgtype,?x) and legal(?o) and neg prior(Kref(?iofluent),?o)). neg legal(?o) :- produces(?o,?m) and message_info(?m,?msgtype,?x) and described_by(?msgtype,?iofluent) and neg prior(Kref(?iofluent),?o)).
Every activity occurrence that reads a message is preceded by an activity occurrence that produces the message.
produces(?o2,m) :- reads(?o1,?m). neg reads(?o1,?m) :- neg produces(?o2,m). precedes(?o2,o1)) :- reads(?o1,?m). neg reads(?o1,?m) :- neg precedes(?o2,o1)).
A message object is created by an activity occurrence that produces a message.
beginof(?m) :=: endof(?o) :- produces(?o,?m). neg produces(?o,?m) :- neg beginof(?m) :=: endof(?o). holds(existing_mobject(?m),?o) :- produces(?o,?m). neg produces(?o,?m) :- neg holds(existing_mobject(?m),?o).
A message object is destroyed by an activity occurrence that destroys a message.
beginof(?m) :=: endof(?o) :- destroys(?o,?m). neg destroys(?o,?m) :- neg beginof(?m) :=: endof(?o). neg holds(existing_mobject(?m),?o) :- destroys(?o,?m). neg destroys(?o,?m) :- holds(existing_mobject(?m),?o).
A ProduceMessage activity is an activity whose occurrences produce messages.
ProduceMessage(?a) :- activity(?a) and neg occurrence_of(_#1(?a),?a). neg activity(?a) :- neg ProduceMessage(?a) and neg occurrence_of(_#1(?a),?a). occurrence_of(_#1(?a),?a) :- neg ProduceMessage(?a) and activity(?a). ProduceMessage(?a) :- activity(?a) and produces(_#1(?a),?m). neg activity(?a) :- produces(_#1(?a),?m) and ProduceMessage(?a). neg produces(_#1(?a),?m) :- neg ProduceMessage(?a) and activity(?a). neg ProduceMessage(?a) :- neg activity(?a). activity(?a) :- ProduceMessage(?a). neg ProduceMessage(?a) :- occurrence_of(?o,?a) and neg produces(?o,_#2(?a,?o)). neg occurrence_of(?o,?a) :- ProduceMessage(?a) and neg produces(?o,_#2(?a,?o)). produces(?o,_#2(?a,?o)) :- ProduceMessage(?a) and occurrence_of(?o,?a).
A ReadMessage activity is an activity whose occurrences read messages.
ReadMessage(?a) :- activity(?a) and neg occurrence_of(_#1(?a),?a). neg activity(?a) :- neg ReadMessage(?a) and neg occurrence_of(_#1(?a),?a). occurrence_of(_#1(?a),?a) :- neg ReadMessage(?a) and activity(?a). ReadMessage(?a) :- activity(?a) and reads(_#1(?a),?m). neg activity(?a) :- reads(_#1(?a),?m) and ReadMessage(?a). neg reads(_#1(?a),?m) :- neg ReadMessage(?a) and activity(?a). neg ReadMessage(?a) :- neg activity(?a). activity(?a) :- ReadMessage(?a). neg ReadMessage(?a) :- occurrence_of(?o,?a) and neg reads(?o,_#2(?a,?o)). neg occurrence_of(?o,?a) :- ReadMessage(?a) and neg reads(?o,_#2(?a,?o)). reads(?o,_#2(?a,?o)) :- ReadMessage(?a) and occurrence_of(?o,?a).
A DestroyMessage activity is an activity whose occurrences destroy messages.
DestroyMessage(?a) :- activity(?a) and neg occurrence_of(_#1(?a),?a). neg activity(?a) :- neg DestroyMessage(?a) and neg occurrence_of(_#1(?a),?a). occurrence_of(_#1(?a),?a) :- neg DestroyMessage(?a) and activity(?a). DestroyMessage(?a) :- activity(?a) and destroys(_#1(?a),?m). neg activity(?a) :- destroys(_#1(?a),?m) and DestroyMessage(?a). neg destroys(_#1(?a),?m) :- neg DestroyMessage(?a) and activity(?a). neg DestroyMessage(?a) :- neg activity(?a). activity(?a) :- DestroyMessage(?a). neg DestroyMessage(?a) :- occurrence_of(?o,?a) and neg destroys(?o,_#2(?a,?o)). neg occurrence_of(?o,?a) :- DestroyMessage(?a) and neg destroys(?o,_#2(?a,?o)). destroys(?o,_#2(?a,?o)) :- DestroyMessage(?a) and occurrence_of(?o,?a).
If a message is contained in a channel, then it is produced by an occurrence of a service that is a source for the channel.
channel_source(?c,_#1(?c,?m)) :- channel_mobject(?c,?m). neg channel_mobject(?c,?m) :- neg channel_source(?c,_#1(?c,?m)). occurrence_of(_#2(?c,?m),_#1(?c,?m)) :- channel_mobject(?c,?m). neg channel_mobject(?c,?m) :- neg occurrence_of(_#2(?c,?m),_#1(?c,?m)). produces(_#3(?c,?m),?m) :- channel_mobject(?c,?m). neg channel_mobject(?c,?m) :- produces(_#3(?c,?m),?m). subactivity_occurrence(_#3(?c,?m),_#2(?c,?m)) :- channel_mobject(?c,?m). neg channel_mobject(?c,?m) :- neg subactivity_occurrence(_#3(?c,?m),_#2(?c,?m)).
If a message is contained in a channel, then it is read by an occurrence of a service that is a target for the channel.
channel_target(?c,_#1(?c,?m)) :- channel_mobject(?c,?m). neg channel_mobject(?c,?m) :- neg channel_target(?c,_#1(?c,?m)). occurrence_of(_#2(?c,?m),_#1(?c,?m)) :- channel_mobject(?c,?m). neg channel_mobject(?c,?m) :- neg occurrence_of(_#2(?c,?m),_#1(?c,?m)). reads(_#3(?c,?m),?m) :- channel_mobject(?c,?m). neg channel_mobject(?c,?m) :- reads(_#3(?c,?m),?m). subactivity_occurrence(_#3(?c,?m),_#2(?c,?m)) :- channel_mobject(?c,?m). neg channel_mobject(?c,?m) :- neg subactivity_occurrence(_#3(?c,?m),_#2(?c,?m)).
Exceptions form a sublcass of fluents.
fluent(e) :- exception(e). neg exception(e) :- neg fluent(e).
The following axioms capture the relationships in Figure 7.
An exception ?e is handled by an activity ?a.
exception(?e) :- is_handled_by(?e,?a). neg is_handled_by(?e,?a) :- neg exception(?e) activity(?a) :- is_handled_by(?e,?a). neg is_handled_by(?e,?a) :- neg activity(?a).
An activity ?a has an exception ?e.
activity(?a) :- has_exception(?a,?e). neg has_exception(?a,?e) :- neg activity(?a). exception(?e) :- has_exception(?a,?e). neg has_exception(?a,?e) :- neg exception(?e).
An activity ?a is an exception-handling activity if and only if it is a TriggeredActivity that there exists an exception that is handled by ?a.
handle_exception(?a) :- is_handled_by(?e, ?a) and TriggeredActivity(?a). neg is_handled_by(?e, ?a) :- neg handle_exception(?a) and TriggeredActivity(?a). neg TriggeredActivity(?a) :- is_handled_by(?e, ?a) and neg handle_exception(?a). is_handled_by(_#1(?a),?a) :- handle_exception(?a). neg handle_exception(?a) :- neg is_handled_by(_#1(?a),?a). TriggeredActivity(?a) :- handle_exception(?a). neg handle_exception(?a) :- neg TriggeredActivity(?a).
find_exception and fix_exception are the two subclasses of exception-handling activities.
handle_exception(?a) :- find_exception(?a). neg find_exception(?a) :- neg handle_exception(?a). handle_exception(?a) :- fix_exception(?a). neg fix_exception(?a) :- neg handle_exception(?a). neg handle_exception(?a) :- neg find_exception(?a) and neg fix_exception(?a). find_exception(?a) :- neg fix_exception(?a) and handle_exception(?a). fix_exception(?a) :- handle_exception(?a) and neg find_exception(?a).
detect_exception and anticipate_exception are the two subclasses of exception-finding activities.
find_exception(?a) :- detect_exception(?a). neg detect_exception(?a) :- neg find_exception(?a). find_exception(?a) :- anticipate_exception(?a). neg anticipate_exception(?a) :- neg find_exception(?a). neg find_exception(?a) :- neg detect_exception(?a) and neg anticipate_exception(?a). detect_exception(?a) :- neg anticipate_exception(?a) and find_exception(?a). anticipate_exception(?a) :- find_exception(?a) and neg detect_exception(?a).
avoid_exception and resolve_exception are the two subclasses of exception-fixing activities.
fix_exception(?a) :- avoid_exception(?a). neg avoid_exception(?a) :- neg fix_exception(?a). fix_exception(?a) :- resolve_exception(?a). neg resolve_exception(?a) :- neg fix_exception(?a). neg fix_exception(?a) :- neg avoid_exception(?a) and neg resolve_exception(?a). avoid_exception(?a) :- neg resolve_exception(?a) and fix_exception(?a). resolve_exception(?a) :- fix_exception(?a) and neg avoid_exception(?a).
The relation is_found_by is the restriction of the is_handled_by relation
to exception-finding activities.
The relation is_fixed_by is the restriction of the is_handled_by relation
to exception-fixing activities.
is_handled_by(?e,?a) :- is_found_by(?e,?a) and find_exception(?a). neg is_found_by(?e,?a) :- neg is_handled_by(?e,?a) and find_exception(?a). neg find_exception(?a) :- neg is_handled_by(?e,?a) and is_found_by(?e,?a). is_handled_by(?e,?a) :- is_fixed_by(?e,?a) and fix_exception(?a). neg is_fixed_by(?e,?a) :- neg is_handled_by(?e,?a) and fix_exception(?a). neg fix_exception(?a) :- neg is_handled_by(?e,?a) and is_fixed_by(?e,?a). neg is_handled_by(?e,?a) :- neg is_found_by(?e,?a) and neg is_fixed_by(?e,?a). is_found_by(?e,?a) :- is_handled_by(?e,?a) and neg is_fixed_by(?e,?a). is_fixed_by(?e,?a) :- is_handled_by(?e,?a) and neg is_found_by(?e,?a). neg is_handled_by(?e,?a) :- neg find_exception(?a) and neg is_fixed_by(?e,?a). find_exception(?a) :- is_handled_by(?e,?a) and neg is_fixed_by(?e,?a). is_fixed_by(?e,?a) :- is_handled_by(?e,?a) and neg find_exception(?a). neg is_handled_by(?e,?a) :- neg is_found_by(?e,?a) and neg fix_exception(?a). is_found_by(?e,?a) :- is_handled_by(?e,?a) and neg fix_exception(?a). fix_exception(?a) :- is_handled_by(?e,?a) and neg is_found_by(?e,?a). neg is_handled_by(?e,?a) :- neg find_exception(?a) and neg fix_exception(?a). find_exception(?a) :- is_handled_by(?e,?a) and neg fix_exception(?a). fix_exception(?a) :- is_handled_by(?e,?a) and neg find_exception(?a). Note: The first triplet of rules is the omnidirectional set for this clause: (a) is_handled_by(?e,?a) or neg is_found_by(?e,?a) or neg find_exception(?a) The second triplet is the omnidirectional set for this clause: (b) is_handled_by(?e,?a) or neg is_fixed_by(?e,?a) or neg fix_exception(?a) The third triplet is the omnidirectional set for this clause: (c) neg is_handled_by(?e,?a) or is_found_by(?e,?a) or is_fixed_by(?e,?a). The fourth triplet is the omnidirectional set for this clause: (d) neg is_handled_by(?e,?a) or find_exception(?a) or is_fixed_by(?e,?a). The fifth triplet is the omnidirectional set for this clause: (e) neg is_handled_by(?e,?a) or is_found_by(?e,?a) or fix_exception(?a). The sixth triplet is the omnidirectional set for this clause: (f) neg is_handled_by(?e,?a) or find_exception(?a) or fix_exception(?a). Clauses (a) and (b) are equivalent to the <== direction of the FLOWS rule. Clauses (c), (d), (e), and (f) are equivalent to the ==> direction of the FLOWS rule.
The relation is_detected_by is the restriction of the is_found_by relation
to exception-detecting activities.
The relation is_anticipated_by is the restriction of the is_found_by relation
to exception-anticipating activities.
is_found_by(?e,?a) :- is_detected_by(?e,?a) and detect_exception(?a). neg is_detected_by(?e,?a) :- neg is_found_by(?e,?a) and detect_exception(?a). neg detect_exception(?a) :- neg is_found_by(?e,?a) and is_detected_by(?e,?a). is_found_by(?e,?a) :- is_anticipated_by(?e,?a) and anticipate_exception(?a). neg is_anticipated_by(?e,?a) :- neg is_found_by(?e,?a) and anticipate_exception(?a). neg anticipate_exception(?a) :- neg is_found_by(?e,?a) and is_anticipated_by(?e,?a). neg is_found_by(?e,?a) :- neg is_detected_by(?e,?a) and neg is_anticipated_by(?e,?a). is_detected_by(?e,?a) :- is_found_by(?e,?a) and neg is_anticipated_by(?e,?a). is_anticipated_by(?e,?a) :- is_found_by(?e,?a) and neg is_detected_by(?e,?a). neg is_found_by(?e,?a) :- neg detect_exception(?a) and neg is_anticipated_by(?e,?a). detect_exception(?a) :- is_found_by(?e,?a) and neg is_anticipated_by(?e,?a). is_anticipated_by(?e,?a) :- is_found_by(?e,?a) and neg detect_exception(?a). neg is_found_by(?e,?a) :- neg is_detected_by(?e,?a) and neg anticipate_exception(?a). is_detected_by(?e,?a) :- is_found_by(?e,?a) and neg anticipate_exception(?a). anticipate_exception(?a) :- is_found_by(?e,?a) and neg is_detected_by(?e,?a). neg is_found_by(?e,?a) :- neg detect_exception(?a) and neg anticipate_exception(?a). detect_exception(?a) :- is_found_by(?e,?a) and neg anticipate_exception(?a). anticipate_exception(?a) :- is_found_by(?e,?a) and neg detect_exception(?a).
The relation is_avoided_by is the restriction of the is_fixed_by relation
to exception-avoiding activities.
The relation is_resolved_by is the restriction of the is_fixed_by relation
to exception-resolving activities.
is_fixed_by(?e,?a) :- is_avoided_by(?e,?a) and avoid_exception(?a). neg is_avoided_by(?e,?a) :- neg is_fixed_by(?e,?a) and avoid_exception(?a). neg avoid_exception(?a) :- neg is_fixed_by(?e,?a) and is_avoided_by(?e,?a). is_fixed_by(?e,?a) :- is_resolved_by(?e,?a) and resolve_exception(?a). neg is_resolved_by(?e,?a) :- neg is_fixed_by(?e,?a) and resolve_exception(?a). neg resolve_exception(?a) :- neg is_fixed_by(?e,?a) and is_resolved_by(?e,?a). neg is_fixed_by(?e,?a) :- neg is_avoided_by(?e,?a) and neg is_resolved_by(?e,?a). is_avoided_by(?e,?a) :- is_fixed_by(?e,?a) and neg is_resolved_by(?e,?a). is_resolved_by(?e,?a) :- is_fixed_by(?e,?a) and neg is_avoided_by(?e,?a). neg is_fixed_by(?e,?a) :- neg avoid_exception(?a) and neg is_resolved_by(?e,?a). avoid_exception(?a) :- is_fixed_by(?e,?a) and neg is_resolved_by(?e,?a). is_resolved_by(?e,?a) :- is_fixed_by(?e,?a) and neg avoid_exception(?a). neg is_fixed_by(?e,?a) :- neg is_avoided_by(?e,?a) and neg resolve_exception(?a). is_avoided_by(?e,?a) :- is_fixed_by(?e,?a) and neg resolve_exception(?a). resolve_exception(?a) :- is_fixed_by(?e,?a) and neg is_avoided_by(?e,?a). neg is_fixed_by(?e,?a) :- neg avoid_exception(?a) and neg resolve_exception(?a). avoid_exception(?a) :- is_fixed_by(?e,?a) and neg resolve_exception(?a). resolve_exception(?a) :- is_fixed_by(?e,?a) and neg avoid_exception(?a).