Skip to content

Commit

Permalink
Merge pull request #460 from AmpersandTarski/development
Browse files Browse the repository at this point in the history
Release 3.5.2
  • Loading branch information
hanjoosten authored Jun 10, 2016
2 parents 4496c8f + c1856ea commit d9b09ee
Show file tree
Hide file tree
Showing 89 changed files with 1,501 additions and 1,526 deletions.
1 change: 1 addition & 0 deletions AmpersandData/FormalAmpersand/AST.adl
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
CONTEXT RAP IN ENGLISH
--! It is allowed to change texts and/or the order of texts IF AND ONLY IF this is also done in the corresponding Haskell files !--
INCLUDE "AST.ifc"
--INCLUDE "MinimalAST.xlsx" -- Contains minimal population. Anything discarded from it must break an invariant
INCLUDE "Contexts.adl"
INCLUDE "Relations.adl"
INCLUDE "Rules.adl"
Expand Down
208 changes: 152 additions & 56 deletions AmpersandData/FormalAmpersand/AST.ifc
Original file line number Diff line number Diff line change
@@ -1,47 +1,105 @@
CONTEXT "AST Interface" IN ENGLISH
CONTEXT "AST Interface" IN ENGLISH

INTERFACE Ampersand FOR Ampersand : I[SESSION];'_SESSION'
TABS[ Context : V[SESSION*Context]
COLS ["name" : name[Context*ContextIdentifier]
, patterns : usedPatterns
]
, "Patterns" : V[SESSION*Pattern]
COLS [ Pattern : name[Pattern*PatternIdentifier]
, Purpose : purpose
, Rules : rules
, Relations : declarations
]
, "Specializations" : V[SESSION*Gen]
COLS [ Generic : gengen
, Specific : genspc
]
, "Concepts" : V[SESSION*PlainConcept]
COLS [ Id: I
-- , Definition : cptdf
-- , Purpose : cptpurpose
-- , "Technical Type" : cpttp
]
, "Relations" : V[SESSION*Relation]
COLS [ name : name
, signature : sign
, properties : decprps;declaredthrough
, pragmaL : decprL
, pragmaM : decprM
, pragmaR : decprR
, Meaning : decmean
, population : in~
]
, "Rules" : V[SESSION*Rule]
COLS [ name : name
, signature : sign
, Expression : rrexp[Rule*Expression]
, Meaning : rrmean
, Purpose : rrpurpose
, Property : declaredthrough
]
-- , "All plugs" : V[ONE*Context];
INTERFACE Ampersand FOR Ampersand : '_SESSION';V[SESSION*Context]
BOX <SHCOLS>
[ "Context" : I
, "name" : name[Context*ContextIdentifier]
]
INTERFACE "Context" FOR Ampersand : I[Context] TABS
[ "About" : I BOX
[ "name" : name[Context*ContextIdentifier]
, "versionInfo" : versionInfo
, "dbName" : dbName
, "owner" : owner[Context*Account]
, "valid~" : valid[Rule*Context]~
]
, "Patterns" : patterns[Context*Pattern] BOX
[ "Pattern" : I INTERFACE Pattern]
, "Gens" : concs ; (I[Concept]
/\
(gengen[Gen*Concept]~;gengen[Gen*Concept]) /\
( -(genspc[Gen*Concept]~;genspc[Gen*Concept])))
INTERFACE GenTree
, "Concepts" : concs[Context*Concept]
, "Relations" : context[Relation*Context]~ LINKTO INTERFACE "Relation"
, "Roles" : allRoles[Context*Role]
, "allConjuncts" : allConjuncts[Context*Conjunct]
, "Rules" : allRules[Context*Rule] INTERFACE "Rule"
]
INTERFACE GenTree FOR Ampersand : I[Concept]
BOX [ concept : I[Concept]
, "Kinds" : gengen~;genspc LINKTO INTERFACE GenTree
]
INTERFACE Pattern FOR Ampersand : I[Pattern]
BOX [ Pattern : name[Pattern*PatternIdentifier]
, "patterns~" : patterns[Context*Pattern]~
, "Relations" : declarations[Pattern*Relation] LINKTO INTERFACE "Relation"
, "rules" : rules[Pattern*Rule]
, "purpose" : purpose[Pattern*Purpose]
]

INTERFACE "Rule" FOR Ampersand : I[Rule]
BOX [ "name" : name[Rule*RuleID]
, "valid" : valid[Rule*Context]
, "allRules~" : allRules[Context*Rule]~
, "originatesFrom~" : originatesFrom[Conjunct*Rule]~
, "rules~" : rules[Pattern*Rule]~
, "maintains~ (Role)" : maintains[Role*Rule]~
, "term (Expression)" : term[Rule*Expression]
, "tgtConcept" : tgtConcept[Rule*Concept]
, "srcConcept" : srcConcept[Rule*Concept]
, "term" : term[Rule*Expression]
, "sign" : sign[Rule*Signature]
, "maintains~ (Plug)" : maintains[Plug*Rule]~
, "origin" : origin[Rule*Origin]
, "rrviols" : rrviols
, "pairView" : pairView
, "message" : message
, "conjunctIds" : conjunctIds
, "rrmean" : rrmean
, "rrpurpose" : rrpurpose
]

INTERFACE "Conjunct" FOR Ampersand : I[Conjunct] BOX
[ "ID" : I
, "originatesFrom" : originatesFrom[Conjunct*Rule]
, "conjunct" : conjunct[Conjunct*Expression]
]
INTERFACE "Concept" FOR Ampersand : I[Concept] BOX
[ concept : I
, name : name
, ttype : ttype
, "source~" : source~ LINKTO INTERFACE Relation
, "target~" : target~ LINKTO INTERFACE Relation
, "gengen~" : gengen~
, "genspc~" : genspc~
, "rootConcept~" : rootConcept~
, "src of expression~" : src[Expression*Concept]~
, "tgt of expression~" : tgt[Expression*Concept]~
, "src of sign~" : src[Signature*Concept]~
, "tgt of sign~" : tgt[Signature*Concept]~
, "concept~" : concept~
, "conceptAttribute" : conceptAttribute
, "in" : in[Concept*Plug]
]

INTERFACE Expression FOR Ampersand : I[Expression]
BOX [ expression: I[Expression]
, first : first LINKTO INTERFACE Expression
, operator : operator
, second : second LINKTO INTERFACE Expression
, arg : arg[UnaryTerm*Expression]
, term : term[Rule*Expression]
, bind : bind LINKTO INTERFACE Expression
, singleton : singleton LINKTO INTERFACE Expression
]
INTERFACE Signature FOR Ampersand : I[Signature]
BOX [ Signature: I[Signature]
, src : src[Signature*Concept] LINKTO INTERFACE "Concept"
, tgt : tgt[Signature*Concept] LINKTO INTERFACE "Concept"
, "sign~ (Relation)" : sign[Relation*Signature]~ LINKTO INTERFACE "Relation"
, "sign~ (Rule)" : sign[Rule*Signature]~ LINKTO INTERFACE "Rule"
]
INTERFACE Atoms FOR Ampersand : I[SESSION];'_SESSION'
TABS[ Atoms : V[SESSION*Atom]
COLS [ "Atom" : I
Expand All @@ -64,25 +122,63 @@ TABS[ Atoms : V[SESSION*Atom]
]



INTERFACE Pattern FOR Ampersand : I[Pattern]
BOX [ Pattern : name[Pattern*PatternIdentifier]
]
INTERFACE PropertyRule FOR Ampersand : I[PropertyRule]
BOX [ "declaredthrough": declaredthrough[PropertyRule*Property]
, "decprps~" : decprps[Relation*PropertyRule]~ LINKTO INTERFACE "Relation"
]



INTERFACE Gen FOR Ampersand : I[Gen]
BOX [ gengen : gengen
, genspc : genspc
BOX [ "gens~" : gens~
, "gengen" : gengen
, "genspc" : genspc
]

INTERFACE Relation FOR Ampersand : I[Relation]
BOX [ name : name
, sign : sign
, decprL : decprL
, decprM : decprM
, decprR : decprR
, meaning : decmean
, purpose : decpurpose
, population: in~
BOX [ "affectedInvConjunctIds" : affectedInvConjunctIds[Relation*Conjunct]
, "affectedSigConjunctIds" : affectedSigConjunctIds[Relation*Conjunct]
, "context" : context[Relation*Context]
, "decmean" : decmean[Relation*Meaning]
, "decprL" : decprL[Relation*String]
, "decprM" : decprM[Relation*String]
, "decprR" : decprR[Relation*String]
, "decprps" : decprps[Relation*PropertyRule]
, "decpurpose" : decpurpose[Relation*Purpose]
, "name" : name[Relation*Identifier]
, "prop" : prop[Relation*Property]
, "sign" : sign[Relation*Signature]
, "source" : source[Relation*Concept]
, "srcAtt" : srcAtt[Relation*SqlAttribute]
, "target" : target[Relation*Concept]
, "tgtAtt" : tgtAtt[Relation*SqlAttribute]
, "bind~" : bind[Expression*Relation]~
, "declarations~" : declarations[Pattern*Relation]~
, "in~" : in[Pair*Relation]~
BOX <SHCOLS>
[ l : l
, r : r
]
, "relations~" : relations[Context*Relation]~
, "relsInPlug~" : relsInPlug[Plug*Relation]~
]
ENDCONTEXT

INTERFACE TblSQL FOR Ampersand : I[TblSQL]
BOX [ "rootConcept" : rootConcept[TblSQL*Concept]
, "key" : key[TblSQL*SqlAttribute]
, "reprType" : reprType[TblSQL*TType]
]
INTERFACE SqlAttribute FOR Ampersand : I[SqlAttribute]
BOX [ "table" : table
, "key~" : key~
, "conceptAttribute~" : conceptAttribute~
, "concept" : concept
, "tgtAtt~" : tgtAtt~
, "srcAtt~" : srcAtt~
]

ENDCONTEXT




Binary file modified AmpersandData/FormalAmpersand/AST.xlsx
Binary file not shown.
5 changes: 3 additions & 2 deletions AmpersandData/FormalAmpersand/Conjuncts.adl
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@ RELATION rc_dnfClauses[Conjunct*DnfClause]
RELATION conjuncts[Rule*Expression]
RELATION expr2dnfClause[Expression*DnfClause] [UNI,TOT]
RELATION allShifts[DnfClause*DnfClause]
RELATION rrexp[Rule*Expression] [UNI,TOT]
--RELATION rrexp[Rule*Expression] [UNI,TOT] HJO: Removed. Is the same as term[Rule*Expression]
RELATION term[Rule*Expression][UNI,TOT] --is defined somewhere else too.
RELATION conjNF[Expression*Expression] [UNI,TOT]
RELATION exprIsc2list[Expression*Expression] [TOT]
RELATION name[Rule*RuleID] [UNI,TOT]
Expand All @@ -19,7 +20,7 @@ MEANING "All conjuncts in a quad are derived by means of the relation ``conjunct
RULE Conjuncts2 : rc_conjunct~;rc_dnfClauses = expr2dnfClause;allShifts
MEANING "A conjunct in a quad stores all dnf-clauses that are derived from the expression in that conjunct."

RULE defconjuncts : conjuncts = rrexp;conjNF;exprIsc2list
RULE defconjuncts : conjuncts = term[Rule*Expression];conjNF;exprIsc2list
MEANING "The conjuncts in a rule are defined as the top-level subexpressions in the conjunctive normal form of the expression related to that rule."

RULE Conjuncts4 : qConjuncts~;qRule |- rc_rulename;name~
Expand Down
4 changes: 2 additions & 2 deletions AmpersandData/FormalAmpersand/Contexts.adl
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,13 @@ PATTERN Context
RELATION name[Context*ContextIdentifier] [UNI,TOT,INJ,SUR]
MEANING "The name of a context."
RELATION valid[Rule*Context]
RELATION usedPatterns[Context*Pattern]
RELATION patterns[Context*Pattern]
MEANING "The patterns in a context."
RELATION concs[Context*Concept]
MEANING "A concept, mentioned anywhere in a context."
RELATION gens[Context*Gen]
MEANING "The user-defined generalization rules in a context."
RELATION relations[Context*Relation] [INJ] -- SUR is maintained by RULE SURrelations
RELATION relations[Context*Relation] [INJ] -- SUR is maintained by RULE SURrelations FIX: Compare with context[Relation*Context]
ENDPATTERN

ENDCONTEXT
Expand Down
Binary file modified AmpersandData/FormalAmpersand/Contexts.xlsx
Binary file not shown.
24 changes: 15 additions & 9 deletions AmpersandData/FormalAmpersand/Expressions.adl
Original file line number Diff line number Diff line change
Expand Up @@ -7,20 +7,17 @@ PROCESS "Expression definitions"
RELATION patterns[Context*Pattern]
RELATION src[Expression*Concept]
RELATION tgt[Expression*Concept]
RELATION lhs[BinaryTerm*Expression]
RELATION rhs[BinaryTerm*Expression]
RELATION bind[Expression*Relation]
RELATION term[Rule*Expression]
RELATION rrexp[Rule*ExpressionID]


VIEW Equivalence : Equivalence(TXT "RULE ", first, TXT " = ", second)
VIEW Inclusion : Inclusion (TXT "RULE ", first, TXT " |- ", second)
VIEW Truth : Truth (TXT "RULE ", I[Expression])
VIEW Relation : Relation(name, TXT "[", source;name, TXT "*", target;name, TXT "]")
VIEW UnaryMinus : UnaryMinus(TXT "-", arg)
VIEW Converse : Converse (arg, TXT "~")
VIEW KleeneStar : KleeneStar(arg, TXT "*")
VIEW KleenePlus : KleenePlus(arg, TXT "+")
VIEW UnaryMinus : UnaryMinus(TXT "-", arg[UnaryTerm*Expression])
VIEW Converse : Converse (arg[UnaryTerm*Expression], TXT "~")
VIEW KleeneStar : KleeneStar(arg[UnaryTerm*Expression], TXT "*")
VIEW KleenePlus : KleenePlus(arg[UnaryTerm*Expression], TXT "+")
VIEW Intersection : Intersection (TXT "(", first, TXT "/\\", second, TXT ")")
VIEW Union : Union (TXT "(", first, TXT "\\/", second, TXT ")")
VIEW Minus : Minus (TXT "(", first, TXT "-" , second, TXT ")")
Expand All @@ -32,7 +29,7 @@ PROCESS "Expression definitions"


CONCEPT Rule ""
RELATION rrexp[Rule*Expression] [UNI]
RELATION term[Rule*Expression] [UNI,TOT]

CONCEPT Operator ""
CONCEPT BinaryTerm ""
Expand All @@ -45,6 +42,15 @@ PROCESS "Expression definitions"
CLASSIFY UnaryTerm ISA Expression
RELATION arg[UnaryTerm*Expression] [UNI]

CONCEPT Atom ""
CLASSIFY Atom ISA Expression
RELATION singleton[Atom*Expression] [UNI]

CONCEPT "V" "The cartesian product."
CLASSIFY "V" ISA Expression
RELATION userSrc["V"*Concept] [UNI]
RELATION userTrg["V"*Concept] [UNI]

CLASSIFY Equivalence ISA Rule
CLASSIFY Inclusion ISA Rule
CLASSIFY Truth ISA Rule
Expand Down
20 changes: 7 additions & 13 deletions AmpersandData/FormalAmpersand/Generics.adl
Original file line number Diff line number Diff line change
Expand Up @@ -17,16 +17,16 @@ RELATION dbName[Context*DatabaseName] [UNI,TOT] -- e.g. 'GRCengine';

--[Relations]--
--IDENT Relations: Relation(name,source,target,context) -- the name of the relation must be unique; it is therefore not the same as a RAP:Relation.
RELATION affectedInvConjunctIds[Relation*ConjunctID]
RELATION affectedInvConjunctIds[Relation*Conjunct]
MEANING "When a pair in a relation is edited (created, updated or deleted), an (invariant) conjunct may be affected"
RELATION affectedSigConjunctIds[Relation*ConjunctID]
RELATION affectedSigConjunctIds[Relation*Conjunct]
MEANING "When a pair in a relation is edited (created, updated or deleted), a (signal) conjunct may be affected"

--[Concepts]--
RELATION name[Concept*Identifier][TOT,UNI]
RELATION affectedInvConjunctIds[Concept*ConjunctID]
RELATION affectedInvConjunctIds[Concept*Conjunct]
MEANING "When an atom in a concept is edited (created, updated or deleted), a (invariant) conjunct may be affected"
RELATION affectedSigConjunctIds[Concept*ConjunctID]
RELATION affectedSigConjunctIds[Concept*Conjunct]
MEANING "When an atom in a concept is edited (created, updated or deleted), a (signal) conjunct may be affected"

--[Rules]--
Expand All @@ -39,7 +39,7 @@ RELATION meaning[Rule*Meaning] -- e.g. 'bfOUprop[BusinessFunction] is antisymmet
RELATION message[Rule*Message] -- e.g. 'bfOUprop[BusinessFunction] is not antisymmetric'
RELATION srcConcept[Rule*Concept][UNI,TOT] -- e.g. 'BusinessFunction'
RELATION tgtConcept[Rule*Concept][UNI,TOT] -- e.g. 'BusinessFunction'
RELATION conjunctIds[Rule*ConjunctID] -- e.g. 'conj_159'
RELATION conjunctIds[Rule*Conjunct] -- e.g. 'conj_159'
RELATION pairView[Rule*PairView] -- e.g.
-- array
-- ( array ( 'segmentType' => 'Text', 'Text' => '{EX} DelPair;rliAcceptableRiskLevel;RLI;')
Expand Down Expand Up @@ -76,14 +76,8 @@ RELATION expSQL[PairViewSegment*MySQLQuery] [UNI] -- IFF SegmentType == 'Exp'

--[Conjuncts]--
RELATION allConjuncts[Context*Conjunct] [SUR,INJ]
RELATION signalRuleNames[Conjunct*Rule] -- e.g. 'Activation of Managed BFControls' -- this is a signal rule
RELATION invariantRuleNames[Conjunct*Rule] -- similar, for invariant rules.
RELATION violationsSQL[Conjunct*MySQLQuery] -- e.g. '/* case: (EIsc lst\\\'@(_:_:_))
-- nhIsDashboard /\\\\ -I[NormHierarchy] ([NormHierarchy*NormHierarchy]) */
-- SELECT DISTINCT isect0.`NormHierarchy` AS `src`, isect0.`tgt_nhIsDashboard` AS `tgt`
-- FROM ( SELECT `NormHierarchy`, `tgt_nhIsDashboard`
-- FROM `NormHierarchy` WHERE `NormHierarchy` IS NOT NULL AND `tgt_nhIsDashboard` IS NOT NULL) AS isect0
-- WHERE isect0.NormHierarchy <> isect0.`tgt_nhIsDashboard` AND isect0.NormHierarchy IS NOT NULL AND isect0.`tgt_nhIsDashboard` IS NOT NULL'
RELATION originatesFrom[Conjunct*Rule] [TOT] -- rule where the conjunct originates from.
RELATION conjunct[Conjunct*Expression] [TOT]

--[Roles]--

Expand Down
Binary file added AmpersandData/FormalAmpersand/MinimalAST.xlsx
Binary file not shown.
2 changes: 1 addition & 1 deletion AmpersandData/FormalAmpersand/Rules.adl
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ REPRESENT RuleID TYPE ALPHANUMERIC
RELATION name[Rule*RuleID] [UNI,TOT,INJ]
MEANING "The name of a rule."
RELATION sign[Rule*Signature] [UNI,TOT]
RELATION rrexp[Rule*Expression] [UNI,TOT]
RELATION term[Rule*Expression] [UNI,TOT]
MEANING "The rule expressed in relation algebra."
RELATION rrmean[Rule * Meaning]
MEANING "The meanings of a rule."
Expand Down
2 changes: 1 addition & 1 deletion AmpersandData/FormalAmpersand/Rules.ifc
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ TABS[ atoms : V[SESSION*Atom]
, rules : V[SESSION*Rule]
COLS [ name : name
, signature : sign
, expression : rrexp
, term : term[Rule*Expression]
, meaning : rrmean
, purpose : rrpurpose
]
Expand Down
Loading

0 comments on commit d9b09ee

Please sign in to comment.