A Z Specification for KRS using Typed Graphs

	specification

	include {graphsZ2.htm}

	| PrimativeConcept, Concept, Individual, Constraint, Rule, Role : NAME

	| shape: ATTRIBUTE_NAME;
	| ellipse, tickedEllipse, rectangle, barredRectangle, roundedRectangle,
	| noSurround: ATTRIBUTE_VALUE;

	| PRIMATIVE_CONCEPT: NODE_COMPONENT
	|----------------
	| PRIMATIVE_CONCEPT.Name = PrimativeConcept;
	| PRIMATIVE_CONCEPT.Level = 2;
	| PRIMATIVE_CONCEPT.Attributes =
	|	{ MakeAttribute(shape,tickedEllipse,0,{LOCKED}) };

	| CONCEPT: NODE_COMPONENT
	|----------------
	| CONCEPT.Name = Concept;
	| CONCEPT.Level = 2;
	| CONCEPT.Attributes = { MakeAttribute(shape,ellipse,0,{LOCKED}) };

	PRIMATIVE_CONCEPT parentof CONCEPT

	| INDIVIDUAL: NODE_COMPONENT
	|----------------
	| INDIVIDUAL.Name = Individual;
	| INDIVIDUAL.Level = 2;
	| INDIVIDUAL.Attributes =
	|	{ MakeAttribute(shape,rectangle,0,{LOCKED}),
	|	  MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED}) };

	| CONSTRAINT: NODE_COMPONENT
	|----------------
	| CONSTRAINT.Name = Constraint;
	| CONSTRAINT.Level = 2;
	| CONSTRAINT.Attributes =
	|	{ MakeAttribute(shape,roundedRectangle,0,{LOCKED}),
	|	  MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED}) };

	| RULE: NODE_COMPONENT
	|----------------
	| RULE.Name = Rule;
	| RULE.Level = 2;
	| RULE.Attributes =
	|	{ MakeAttribute(shape,barredRectangle,0,{LOCKED}),
	|	  MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED}) };

	| ROLE: NODE_COMPONENT
	|----------------
	| ROLE.Name = Role;
	| ROLE.Level = 2;
	| ROLE.Attributes =
	|	{ MakeAttribute(shape,noSurround,0,{LOCKED}),
	|	  MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED}) };

	| hasConstraint: ARC_COMPONENT
	|----------------
	| hasConstraint.Level = 2;
	| hasConstraint.Attributes = 
	|	{MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED})};
	| (arc~(hasConstraint.Role)).Terminals = << MakeTerminal(ROLE,FROM),
	|				            MakeTerminal(CONSTRAINT,TO) >>;

	| hasValue: ARC_COMPONENT
	|----------------
	| hasValue.Level = 2;
	| hasValue.Attributes = 
	|	{MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED})};
	| (arc~(hasValue.Role)).Terminals = << MakeTerminal(ROLE,FROM),
	|				         MakeTerminal(INDIVIDUAL,TO) >>;

	| hasRole: ARC_COMPONENT
	|----------------
	| hasRole.Level = 2;
	| hasRole.Attributes = 
	|	{MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED})};
	| (arc~(hasRole.Role)).Terminals = << MakeTerminal(PRIMATIVE_CONCEPT,FROM),
	|				      MakeTerminal(ROLE,TO) >>;

	| ifThen: ARC_COMPONENT
	|----------------
	| ifThen.Level = 2;
	| ifThen.Attributes = 
	|	{MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED})};
	| (arc~(ifThen.Role)).Terminals = << MakeTerminal(CONCEPT,FROM),
	|				     MakeTerminal(RULE,TO) >>;

	| hasRoleR: ARC_COMPONENT
	|----------------
	| hasRoleR.Level = 2;
	| hasRoleR.Attributes = 
	|	{MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED})};
	| (arc~(hasRoleR.Role)).Terminals = << MakeTerminal(RULE,FROM),
	|				       MakeTerminal(ROLE,TO) >>;

	| exceptionTo: ARC_COMPONENT
	|----------------
	| exceptionTo.Level = 2;
	| exceptionTo.Attributes = 
	|	{MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED})};
	| (arc~(exceptionTo.Role)).Terminals = << MakeTerminal(RULE,FROM),
	|				          MakeTerminal(RULE,TO) >>;

	| exclusive: ARC_COMPONENT
	|----------------
	| exclusive.Level = 2;
	| exclusive.Attributes = 
	|	{MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED})};
	| (arc~(exclusive.Role)).Terminals = << MakeTerminal(PRIMATIVE_CONCEPT,FROM),
	|				        MakeTerminal(PRIMATIVE_CONCEPT,FROM) >>;

	| coreferent: ARC_COMPONENT
	|----------------
	| coreferent.Level = 2;
	| coreferent.Attributes = 
	|	{MakeAttribute(parentOfIndividual,NULLav,0,{LOCKED})};
	| (arc~(coreferent.Role)).Terminals = << MakeTerminal(PRIMATIVE_CONCEPT,TO),
	|				         MakeTerminal(PRIMATIVE_CONCEPT,TO) >>;

	KRSTypes == {PRIMATIVE_CONCEPT, CONCEPT, INDIVIDUAL, CONSTRAINT, RULE, ROLE}

	KRSRelations == {hasConstraint, hasValue, hasRole, ifThen, hasRoleR,
		         exceptionTo, exclusive, coreferent}

	Level2Objects == KRSTypes || KRSRelations

	---KRS_GRAPH-------------------------------------------------------------
	| FIRST_ORDER_TYPED_GRAPH
	|-------------
	| Level2Objects subset Contents;
	| % There are no other Level 2 objects
	| forall c:Contents |
	|	c notin (Level2Objects||Level1Objects) /\ not(c isa ISA) @
	|		c.Level>2 /\
	| % Every higher level object must have a KRSType parent
	|		(exists1 c2:KRSTypes @ c isa c2);
	------------------------------------------------------------------------

	end specification