CONTEXT RAP 
-- HJO, 20140212: Begin gemaakt met het 'ontmantelen' van dit bestand. Het is de bedoeling om het te splitsen in het 'core' deel van Ampersand (FormalAmpersand.adl) en het overige deel, dat nodig is voor de Repository tool (ADLTool.adl)

INCLUDE "student_AST_interfaces.adl"
INCLUDE "admin_interfaces.adl"
INCLUDE "Fspec.adl"
--IN ENGLISH
--LATEX

PROCESS AtlasLoad
ROLE Student MAINTAINS parseerror,typeerror,popchanged
--TODO -> BUG1 => only  inios = cptos does not imply  inios |- cptos, thus removal of concept population is not detected by conceptwijzigingen.
-- workaround = two rules
--TODO -> BUG2 => removal of cptos results in KEY AtomID => <KEY relation not total>
--RULE "conceptwijzigingen": inios = cptos
--MESSAGE "U heeft wijzigingen gemaakt in de populatie van concepten, die nog niet effectief en persistent opgeslagen zijn. Mogelijk heeft u overtredingen verholpen of veroorzaakt. U kunt deze atlasbewerkingen effectueren en persistent maken door ze op te slaan in een volgende versie van het bronbestand."
--RULE "conceptwijzigingen1": inios |- cptos
--MESSAGE "U heeft atomen verwijderd uit de populatie van concepten, hetgeen nog niet effectief en persistent opgeslagen is. Mogelijk heeft u overtredingen verholpen of veroorzaakt. U kunt deze atlasbewerkingen effectueren en persistent maken door ze op te slaan in een volgende versie van het bronbestand."
--RULE "conceptwijzigingen2": cptos |- inios
--MESSAGE "U heeft atomen toegevoegd aan de populatie van concepten."

--RULE "popadd": (left;atomvalue)~;(decpopu~;decpopu /\ I);right;atomvalue |- inileft~;(inipopu~;inipopu /\ I);iniright
--RULE "popdel": inileft~;(inipopu~;inipopu /\ I);iniright |- (left;atomvalue)~;(decpopu~;decpopu /\ I);right;atomvalue
RULE "popchanged": inipopu = decpopu
--RULE "popchanged": (-((left;atomvalue)~;(decpopu~;decpopu /\ I);right;atomvalue) \/ (inileft~;(inipopu~;inipopu /\ I);iniright)) /\ (-(inileft~;(inipopu~;inipopu /\ I);iniright) \/ ((left;atomvalue)~;(decpopu~;decpopu /\ I);right;atomvalue))
MESSAGE "<br/>You entered change(s) on the screen. You can: <br/> 1) <b>enter more</b> change(s), or; <br/> 2) <b>undo</b> your changes <b>by (re)loading</b> any CONTEXT into Atlas, or;<br/> 3) <a href='index.php?interface=Validate&atom=1&role=0'>click here</a> to <b>commit</b> the change(s) <b>and update</b> violations on your rules."
VIOLATION (TXT "added or deleted pair ",TGT I, TXT " of ", TGT (inipopu\/decpopu)~)


RULE "parseerror": parseerror |- -parseerror
MESSAGE "<span class='errsignal'>A syntax error was encountered in your script.</span> No CONTEXT screen could be generated."
VIOLATION (TGT I, TXT " Open ", SRC I,TXT " to fix error.")

RULE "typeerror": typeerror |- -typeerror
MESSAGE "<span class='errsignal'>Type error(s) were encountered in your script.</span> A CONTEXT screen was generated with concepts and relation declarations only, which may be useful to understand and fix the errors"
VIOLATION (TGT I, TXT ". Open ", SRC I,TXT " to fix error.")
ENDPROCESS

PROCESS Student
ROLE Student MAINTAINS otherviolations, multviolations1,multviolations2,multviolations3, homoviolations

--RULE "conceptorphan": cptos |- src~;decsgn~;decpopu;left \/ trg~;decsgn~;decpopu;right
--MESSAGE "<br/><span class='warnsignal'>The atoms below are not related to any atom, besides the identity relation.</span> These atoms have no purpose to exist, except when the atom is used in a RULE assertion. An atom that has lost its purpose will not exist anymore in the next CONTEXT version if you <a href='index.php?interface=Validate&atom=1&role=0'>Validate</a> now."
--VIOLATION (TGT I)

--RULE "specgenduplicate": -(cptos;atomvalue /\ (genspc~;gengen \/ genspc~;gengen;genspc~;gengen \/ genspc~;gengen;genspc~;gengen;genspc~;gengen)~;cptos;atomvalue)
--MESSAGE "<span class='warnsignal'>Atom(s) of a concept that is a specialization have the same name(s) as atom(s) of a more general concept.</span> The integrity rules demand that no two atoms in the population of a concept have the same name. If you commit and validate on the <a href='index.php?interface=Validate&atom=1&role=0'>Validate-screen</a> then Ampersand records that the atoms with identical names refer to the same real-world object. If the atoms refer to different real-world objects, then you must change the name of at least one atom before validating."
--VIOLATION (TXT "Atom ", TGT I, TXT "will become the most specific concept")

RULE "multviolations1": -((I[PropertyRule] /\ declaredthrough;('TOT' \/ 'SUR');declaredthrough~);rrviols)
MESSAGE "<br/><br/><span class='violsignal'>A TOTal or SURjective multiplicity rule is violated for some relation(s).</span> Add tuple(s) in the relation(s) to correct the violation(s)."
VIOLATION (TXT "RULE ", SRC I, TXT " is violated by the atom ", TGT left, TXT ".")

RULE "multviolations2": -((I[PropertyRule] /\ declaredthrough;('UNI' \/ 'INJ');declaredthrough~);rrviols)
MESSAGE "<br/><br/><span class='violsignal'>A UNIvalence or INJective multiplicity rule is violated for some relation(s).</span> Delete tuple(s) in the relation(s) to correct the violation(s)."
VIOLATION (TXT "RULE ",SRC I, TXT " is violated by the tuple ", TGT I, TXT " in combination with some other tuple(s).")

RULE "multviolations3": -((I[PropertyRule] /\ declaredthrough;'->';declaredthrough~);rrviols)
MESSAGE "<br/><br/><span class='violsignal'>A UNIvalence or TOTal multiplicity rule is violated for some relation(s).</span> Delete tuple(s) in the relation(s) to correct the violation(s)."
VIOLATION (TXT "RULE ",SRC I, TXT " is violated by the tuple ", TGT I, TXT " in combination with some other tuple(s).")

RULE "homoviolations": -((I[PropertyRule] /\ declaredthrough;('RFX' \/ 'IRF' \/ 'SYM' \/ 'ASY' \/ 'TRN' \/ 'PROP');declaredthrough~);rrviols)
MESSAGE "<br/><br/><span class='violsignal'>A rule for homogeneous relation(s) is violated.</span> Add or delete tuple(s) in the relation(s) to correct the violation(s)."
VIOLATION (TXT "RULE ",SRC I, TXT " is violated by the tuple ", TGT I, TXT " in combination with some other tuple(s).")

RULE "otherviolations": -((-I[PropertyRule] /\ I[Rule]);rrviols)
MESSAGE "<br/><br/><span class='violsignal'>A business rule that involves several relations is violated.</span> Add or delete tuple(s) in one or more of the relation(s) to correct the violation(s)."
VIOLATION (TXT "RULE ",SRC I[Rule], TXT " is violated by the violation ", TGT I, TXT " in combination with some other tuple(s).")
ENDPROCESS

PROCESS Admin
--no signals for admin yet
RULE dummy: firstloadedwith |- firstloadedwith
ROLE Admin MAINTAINS dummy
ENDPROCESS


PATTERN AtlasLoad
firstloadedwith :: AdlFile * AdlVersion [UNI]
MEANING IN ENGLISH "The version of the Ampersand compiler with which the rule specification file was loaded for the first time."
inios::Concept*AtomID
MEANING IN ENGLISH "The initial population of a concept from a rule specification file."
inipopu::Declaration*PairID
MEANING IN ENGLISH "The initial population of a relation from a rule specification file."
inileft::PairID*Atom
MEANING IN ENGLISH "The initial source of a relationship from the initial population of a relation from a rule specification file."
iniright::PairID*Atom
MEANING IN ENGLISH "The initial target of a relationship from the initial population of a relation from a rule specification file."
CONCEPT ErrorMessage "An error message is a description of an error." TYPE "Blob"
KEY ParseError: ParseError(TXT "Click here for error details.")
parseerror   :: File * ParseError[UNI]
MEANING IN ENGLISH "The parse error resulting from the parser of the Ampersand compiler when the rule specification file was loaded for the first time."
pe_action    :: ParseError -> String
MEANING IN ENGLISH "Possible actions which may resolve a parse error."
pe_position  :: ParseError -> String
MEANING IN ENGLISH "The position of a parse error."
pe_expecting :: ParseError -> ErrorMessage
MEANING IN ENGLISH "A message of what was expected by the parser."
KEY TypeError: TypeError(TXT "Click here for details of error at ", te_position)
typeerror   :: File * TypeError
MEANING IN ENGLISH "The type error resulting from the type checker of the Ampersand compiler when the rule specification file was loaded for the first time."
te_message  :: TypeError * ErrorMessage [UNI]
MEANING IN ENGLISH "A complete description of a type error."
te_parent   :: TypeError * TypeError [UNI]
MEANING IN ENGLISH "The parent type error of a nested type error."
te_position :: TypeError * String [UNI]
MEANING IN ENGLISH "The position of a type error."
te_origtype :: TypeError * String [UNI]
MEANING IN ENGLISH "The type of element in which the type error has been detected."
te_origname :: TypeError * String [UNI]
MEANING IN ENGLISH "The name of the element in which the type error has been detected."
ENDPATTERN

PATTERN FileManagement
filename :: File->FileName
MEANING IN ENGLISH "The name of a file"
filepath :: File*FilePath[UNI]
MEANING IN ENGLISH "The path of a file"
KEY File: File(PRIMHTML "<a href='../../index.php?file=", filepath, filename,PRIMHTML "&userrole=", uploaded~;userrole, PRIMHTML "'>", filename, PRIMHTML "</a>")
RULE "unique file location": filename;filename~ /\ filepath;filepath~ |- I
MEANING IN ENGLISH "Each file has its own location on the file system."

filetime :: File*CalendarTime[UNI]
MEANING IN ENGLISH "The last time a file has been updated. In RAP this is the creation date, because files may not be edited or overwritten."

uploaded::User*File
MEANING IN ENGLISH "The files in RAP uploaded by a student"
userrole::User*Role [UNI]
MEANING IN ENGLISH "The current role of a mainstream user."
RULE "user roles": 'Student' \/ 'StudentDesigner' \/ 'Designer' |- I[Role]
MEANING IN ENGLISH "There are three roles: Student, StudentDesigner and Designer"

SPEC AdlFile ISA File
--KEY AdlFile: inherit from File
sourcefile::Context->AdlFile
MEANING IN ENGLISH "The rule specification file in which a context is defined."
includes  ::Context*File
MEANING IN ENGLISH "The files included by the main rule specification file of a context."

applyto::G->AdlFile
MEANING IN ENGLISH "The application of an Ampersand compiler function (G) to a rule specification file."
functionname :: G->String
MEANING IN ENGLISH "The description of the application of an Ampersand compiler function to a rule specification file."
operation :: G->Int
MEANING IN ENGLISH "The operation number of an Ampersand compiler function."
KEY G: G(PRIMHTML "<a href='../../index.php?operation=",operation
        ,PRIMHTML "&file=", applyto;filepath , applyto;filename
        ,PRIMHTML "&userrole=", applyto;uploaded[User*AdlFile]~;userrole
        ,PRIMHTML "'>", functionname, PRIMHTML "</a>")


SPEC NewAdlFile ISA AdlFile
KEY NewAdlFile: NewAdlFile(PRIMHTML "<a href='../../index.php'>",filename[NewAdlFile*FileName],PRIMHTML"</a>")
newfile::User->NewAdlFile
MEANING IN ENGLISH "The predefined rule specification file with an empty context, which is copied to create a new file requested by a student."

SPEC SavePopFile ISA File
KEY SavePopFile: SavePopFile(PRIMHTML "<a href='../../index.php?operation=4&file=", filepath[SavePopFile*FilePath] , filename[SavePopFile*FileName]
                            ,PRIMHTML "'>", filename[SavePopFile*FileName] ,PRIMHTML "</a>")
savepopulation::Context->SavePopFile
MEANING IN ENGLISH "The file, which will be created to export the population of a context when requested by a student."

SPEC SaveAdlFile ISA AdlFile
KEY SaveAdlFile: SaveAdlFile(PRIMHTML "<a href='../../index.php?operation=2&file=", filepath[SaveAdlFile*FilePath] , filename[SaveAdlFile*FileName]
                            ,PRIMHTML "&userrole=", savecontext~;sourcefile;uploaded[User*AdlFile]~;userrole
                            ,PRIMHTML "'>", filename[SaveAdlFile*FileName], PRIMHTML "</a>")
savecontext::Context->SaveAdlFile
MEANING IN ENGLISH "The rule specification file, which will be created to commit and upload changes in the loaded context when requested by a student."
ENDPATTERN

PATTERN Metrics
countrules :: Context*Int[UNI]
MEANING IN ENGLISH "The number of user-defined rules in a context"
countdecls :: Context*Int[UNI]
MEANING IN ENGLISH "The number of user-declared relations in a context"
countcpts  :: Context*Int[UNI]
MEANING IN ENGLISH "The number of concepts in a context"
ENDPATTERN

ENDCONTEXT