(* Specifications for the Inferno Process Manager - R. Scovil Fall '98
 *  Given that the "PM" is intentionally similar to other pieces of Inferno,
 *  aspects of those other pieces will be utilized here in order to benefit
 *  from their code base, help ensure similar functionality, and prevent
 *  inadvertent re-invention of spurious wheels.
 *)

(*
 * The following has brought in from the Process Navigator's process.rsl
 *  at the suggestion of G. Fisher - they are outside the constraints of any module
 *  [as are any objects derived from them] and hence are global for the purposes
 *  of this specification
 *************************************************
 * Module Process defines the objects and operations of the software process,
 * as presented to the user through the Procomatic UI.
 *)


(*
  from Standard import Name[*, TextId *];
  from Artifact import Artifact, TextArtifact, GraphicArtifact, TextId;
  from ToolEnvir import Tool, Tools, ToolId;
  export Process, ProcessStep;
*)
  (*
   * Move TextId out of Artifact and into Standard because we wish to import
   * it here instead of name
   *)

(* Declare normally imported Name, TextId so this will compile *)

  obj TextId is string;

  obj Name is TextId;


  obj Transition is 
    TransitionExecutionAttributes and
    PreviousStep and
    NextStep and
    TextId

    description: (*
	The "pipe" between two process steps.  Used only to represent
	dataflow attributes (see TransitionExecutionAttribute). 

	Note:  Porcelli is still a bit fuzzy on how exactly this thing
	is going to work, although he feels comfortable with its existence
	now (in its current form).  The problem is one of location.  
	Currently, process steps do not actually refer to transitions.
	This may need to change.

	Note2:  Can PreviousStep and NextStep be used here even though
	they are "meant" for the ProcessStep, or should other objects be
	defined to basically perform the same function here?
    *);
  end;

  obj TransitionExecutionAttributes is TransitionExecutionAttribute*
    description: (*
	Unordered collection of TransitionExecutionAttributes.
    *);
  end;

  obj TransitionExecutionAttribute
    description: (*
        Attributes of transition as part of an executable process.  E.g.,
        dataflow attributes such as historical, stream, etc.
    *);
  end;

  obj Process is ProcessStepList
    description: (*
	This is a software process.
    *);
  end;

  obj ProcessStepList is ProcessStep*
    description: (*
	This is an ordered collection of ProcessSteps.
    *);
  end;

  obj ProcessStep is
    name: ProcessStepName and
    prev: PreviousStep and
    next: NextStep and
    ia:   InputArtifact and
    outa: OutputArtifact and
    prec: Precondition and
    pstc: Postcondition and
    inv:  Invariant and
    tool: ApplicableTool and
    pss:  ProcessSubSteps and
    ip:   IsPervasive and
    iip:  IsInstantiatedPervasive and
    isa:  IsAutomated and
    ise:  IsEnforced and
    ispc: IsPartiallyCompletable and
    isdr: IsDirectlyReenterable and
    perm: Permissions and
    a:    Appearance and (* infections... mike wants it out of here *)
    apo:  AutomatedProcessOperation  

    description: (*
	This is a substep of a software process.  It can be composed of 
	further process sub-steps, but it need not be.
    *);
  end;

  obj ProcessStepName is TextId
    description: (*
	This is the name of the process step.

	Note:  Porcelli is wondering why this is not simply a TextID like
	it is for Artifacts.
    *);
  end;

  obj PreviousStep is ProcessStepName
    description: (*
	This is the name of the previous step in the process.
    *);
  end;

  obj NextStep is ProcessStepName
    description: (*
	This is the name of the following step in the process
    *);
  end;

  obj InputArtifact is TextId
    description: (*
	An input artifact is the textual id of the artifact that a particular
	process step inputs.  That is, the text id specifies the path into THE
	artifact.
    *);
  end;

  obj OutputArtifact is TextId
    description: (*
	An output artifact is the textual id of the artifact that a particular
	process step outputs.  That is, the text id specifies the path into THE
	artifact.
    *);
  end;

  obj Precondition
    description: (*
	This is what should be true prior to the enactment of this process
	step.  It will involve the status of THE artifact.  It has yet to
	be formally defined.

	Note:  Porcelli is wondering a number of things
        - is this necessary given the existence of the post-condition of the 
	  previous step.  
	- should there be some sort of enforcement of it?
        - do PartiallyCompletable and DirectlyReenterable effect this in any
	  way?  
    *);
  end;

  obj Postcondition
    description: (*
	This is what should be true after the enactment of this process step.
	It will involve the status of THE artifact.  It has yet to be
	formally defined.  However we do know this about it:  if IsEnforced
	is true then the process enactment engine will prevent the 
	NextStep from being enacted until the Postcondition is met.
    *);
  end;

  obj Invariant
    description: (*
	This is what should be true during the enactment of this process step.
	It will involve the status of THE artifact.  It has yet to be
	formally defined.
    *);
  end;

  obj ApplicableTool is Tool
    description: (*
	An applicable tools list is an explicit list of tools that are
	applicable to (i.e., lauchable from) a process step.  If this list is
	empty for a given step, then the applicable tools are all those that
	output the same type of artifact that the process step outputs (see
	SelectForLaunch operation below).
    *);
  end;

  obj ProcessSubSteps is ProcessStepList
    description: (*
	Process substeps are just recursively more of the same.  The hiearchy
	stops when the substeps for a given step are nil.
    *);
  end;

  obj IsPervasive is boolean
    description: (*
	That a process step is pervasive means that it automatically 
	follows all proces steps.  For us, testing is such process step.
	For others it may not be.  Note that we have yet to define formally
	(enough) what "between other steps" means.
    *);
  end;

  obj IsInstantiatedPervasive is boolean
    description: (*
    *);
  end;

  obj IsAutomated
    description: (*
	The automated level of process execution means that there is a fully
	automatic operation that converts the step's input to its output.
        I.e., the step has a "compiler" that performs its operation.
    *);
  end;

  obj IsEnforced is boolean
    description: (*
	If this is true, then the enactment engine prevents the enactment
	of the NextStep until the PostCondition is true.  If it is
	false, then the enactment engine allows the enactment of the
	NextStep even if the Postcondition is false.
    *);
  end;

  obj IsPartiallyCompletable is boolean
    description: (*
	If this is true, then the enactment engine allows any process step
	prior to this one that IsDirectlyReenterable to be enacted.  Even
	if this ProcessStep IsEnforced, the enactment engine will allow
	the enactment of prior process steps that are DirectlyReenterable
	even if the current ProcessStep IsEnforced.  If the current 
	ProcessStep IsEnforced and is NOT PartiallyCompletable, then the
	enactment engine allows only enactment of the current process step
	and no others until the Postcondition is true.

	Note:  'prior to' must be formalized
    *);
  end;

  obj IsDirectlyReenterable is boolean
    description: (*
	
    *);
  end;

  obj Permissions is
    ReadPermission or
    WritePermission or
    ExecutePermission

   description: (*
	Specific interpretations of the three possible permission settings
	will be defined by operations take ProcessSteps as input.  For example:
	the navigate will interpret read permission as the definition as
	to whether  is allowed to navigate to a particular step.  The enactment
	operation will interprete as the definition as to whether a user is
	allct a particular step.  The process definition will interpret write

	permission as the definition as to whether a allowed to modify a 
	particular ProcessStep (where modification included deletion).
   *);
   end;

  obj ReadPermission;
  obj WritePermission;
  obj ExecutePermission;
	
  obj Appearance is GraphicArtifact
    description: (*
    *);
  end;

  obj AutomatedProcessOperation is op(Artifact)->(Artifact)
    description: (*
	An Automated ProcessOperation is an operation type, with the same
	signature as a tool.  This is the operation that fully automates the
	process step's output.  For example, the first design process substep
	that automatically converts an RSL spec to a gross C++ design is such a
	process operation.  Non-automated production of process step output is
	carried out by user-lauchned tools (see specs of ApplicableTool and
	SelectForLaunch below  
    *);
  end;

  (*
   * The following axiom captures the conceuptal meaning of "pervasive process
   * step", which is that in a given process, pervasive steps automatically
   * exist between all ordered steps in that process.
   *)
  axiom
    forall (p:Process, ps:ProcessStep, pps:ProcessStep |
            (ps.ip = false) and           (* ps is a non-pervasive step *)
            (pps.ip = true) and           (* pps is a pervasive step *)
            (ps in p) and (pps in p))      (* both ps and pps are in p *)
    (
        exists (ppsi:ProcessStep |
            (ppsi.iip = true)  and        (* ppsi is an *) 
            (ppsi in p))                  (* instantiated pervasive step in p*)
        (
            (ppsi.prev = ps.name) and     (* ppsi is between ps and *)
            (ppsi.next = ps.next) and     (*   ps's next step, and *)
            (OtherwiseEqual(pps, ppsi))   (* pps and ppsi are otherwise equal*)
        )
    );


  (*
   * Function OtherwiseEqual asserts that an uninstantiated pervasive process
   * step and one of its instantiated counterparts are equal except for
   * certain fields, such as next and previous.
   *)
  function OtherwiseEqual(ps:ProcessStep, pps:ProcessStep) = ... ;


  (*
   * From here down to be completed by Hayley Zhang as part of her work
   * for CSC 510, Fall, 1997
   *)

  obj AnalyzeStep:ProcessStep =
  {
    "Analyze", AnalyzeTool, AnalysisSubSteps, false
  }
  end;

  obj PerformGeneralRequirementsAnalysisStep:ProcessStep =
  {
    "PerformGeneralRequirementsAnalysis"
  }
  end;

  obj StateProblemsToBeSolvedStep:ProcessStep =
  {
    "StateProblemsToBeSolved"
  }
  end;

  obj IdentifyPeopleInvolvedStep:ProcessStep = 
  {
    "IdentifyPeopleInvolved"
  }
  end;

  obj AnalyzeCurrentStateOfOperationsStep:ProcessStep =
  {
    "AnalyzeCurrentStateOfOperationsStep"
  }
  end;

  obj DefineFunctionalRequirementsStep:ProcessStep =
  {
    "DefineFunctionalRequirementsStep"
  }
  end;

  obj InterviewCustomersStep:ProcessStep =
  {
    "InterviewCustomersStep"
  }
  end;

  obj DoScenariosStep:ProcessStep =
  {
    "DoScenariosStep"
  }
  end;

  obj DefineGoalsConstraintsAndNonFunctionalRequirementsStep:ProcessStep =
  {
    "DefineGoalsConstraintsAndNonFunctionalRequirementsStep"
  }
  end;

  obj AnalyzeMarketStep:ProcessStep =
  {
    "AnalyzeMarketStep"
  }
  end;

  obj SurveyPotentialMarketCustomersStep:ProcessStep =
  {
    "SurveyPotentialMarketCustomersStep"
  }
  end;

  obj PerformCustomerDemographicAnalysisStep:ProcessStep =
  {
    "PerformCustomerDemographicAnalysisStep"
  }
  end;

  obj PerformCostBenefitRiskAnalysisStep:ProcessStep =
  {
    "PerformCostBenefitRiskAnalysisStep"
  }
  end;

  obj SpecifyStep:ProcessStep = 
  {
    "Specify", SpecTool, SpecificationSubSteps, false
  }
  end;

  obj DefineObjectsStep:ProcessStep =
  {
    "DefineObjectsStep"
  }
  end;

  obj DefineOperationsStep:ProcessStep =
  {
    "DefineOperationStep"
  }
  end;

  obj DefineObjectEquationsStep:ProcessStep =
  {
    "DefineObjectEquationsStep"
  }
  end;

  obj DefineOperationPreconditionAndPostconditionStep:ProcessStep =
  {
    "DefineOperationPreconditionAndPostconditionStep"
  }
  end;

  obj DefineOtherObjectAndOperationAttributesStep:ProcessStep =
  {
    "DefineOtherObjectAndOperationAttributesStep"
  }
  end;

  obj DefineGlobalAxiomsStep:ProcessStep =
  {
    "DefineGlobalAxiomsStep"
  }
  end;

  obj DefineAndProvePutativeTheoremsStep:ProcessStep =
  {
    "DefineAndProvePutativeTheoremsStep"
  }
  end;

  obj PrototypeStep:ProcessStep = 
  {
    "Prototype", PrototypeTool, PrototypeSubsteps, false
  }
  end;

  obj RefineScenarioStoryboardsIntoUIScreensStep:ProcessStep =
  {
    "RefineScenarioStoryboardsIntoUIScreensStep"
  }
  end;

  obj SensitizeUIScreensStep:ProcessStep =
  {
    "SensitizeUIScreensStep"
  }
  end;

  obj WritePrototypeScriptsStep:ProcessStep =
  {
    "WritePrototypeScriptsStep"
  }
  end;

  obj DesignStep:ProcessStep =
  {
    "Design", DesignTool, DesignSubSteps, false
  }
  end;

  obj DeriveInitialDesignFromSpecificationStep:ProcessStep =
  {
    "DeriveInitialDesignFromSpecificationStep"
  }
  end;

  obj DefineSubsystemModulesInBlockDiagramsStep:ProcessStep =
  {
    "DefineSubsystemModulesInBlockDiagramsStep"
  }
  end;

  obj DefineHighLevelControlFlowInDFDsStep:ProcessStep =
  {
    "DefineHighLevelControlFlowInDFDsStep"
  }
  end;

  obj DeriveInitialFunctionDiagramFromDFDsStep:ProcessStep =
  {
    "DeriveInitialFunctionDiagramFromDFDsStep"
  }
  end;

  obj DefineClassesStep:ProcessStep =
  {
    "DefineClassesStep"
  }
  end;

  obj AssociateFunctionWithClassesStep:ProcessStep =
  {
    "AssociateFunctionWithClassesStep"
  }
  end;

  obj ObjectifyFunctionSignaturesStep:ProcessStep =
  {
    "ObjectifyFunctionSignaturesStep"
  }
  end;

  obj RefineFunctionsPreconditionAndPostconditionsStep:ProcessStep =
  {
    "RefineFunctionsPreconditionAndPostconditionsStep"
  }
  end;

  obj DefineClassMemberVisibilityStep:ProcessStep =
  {
    "DefineClassMemberVisibilityStep"
  }
  end;

  obj DefineClassInheritanceAndRelationsInDataDiagramsStep:ProcessStep =
  {
    "DefineClassInheritanceAndRelationsInDataDiagramsStep"
  }
  end;

  obj DefineModularizationStep:ProcessStep =
  {
    "DefineModularizationStep"
  }
  end;

  obj ApplyMVPMethodologyStep:ProcessStep =
  {
    "ApplyMVPMethodologyStep"
  }
  end;

  obj ApplyHIPOMethodologyStep:ProcessStep =
  {
    "ApplyHIPOMethodologyStep"
  }
  end;

  obj ApplyClientServerMethodologyStep:ProcessStep =
  {
    "ApplyClientServerMethodologyStep"
  }
  end;

  obj RefineNewlyDefinedClassesStep:ProcessStep =
  {
    "RefineNewlyDefinedClassesStep"
  }
  end;

  obj DefineFunctionPreconditionsAndPostconditionsStep:ProcessStep =
  {
    "DefineFunctionPreconditionsAndPostconditionsStep"
  }
  end;

  obj DefineClassMemberVisibilitysStep:ProcessStep =
  {
    "DefineClassMemberVisibilitysStep"
  }
  end;

  obj DefineClassInheritancesAndRelationsInDataDiagramsStep:ProcessStep =
  {
    "DefineClassInheritancesAndRelationsInDataDiagramsStep"
  }
  end;

  obj DefineExceptionHandlingStep:ProcessStep =
  {
    "DefineExceptionHandlingStep"
  }
  end;

  obj DefineEventHandlingStep:ProcessStep =
  {
    "DefineEventHandlingStep"
  }
  end;

  obj ApplyDesignHeuristicsStep:ProcessStep =
  {
    "ApplyDesignHeuristicsStep"
  }
  end;

  obj MinimizeCouplingStep:ProcessStep =
  {
    "MinimizeCouplingStep"
  }
  end;

  obj MaximizeCohesionStep:ProcessStep =
  {
    "MaximizeCohesionStep"
  }
  end;

  obj DefineSCOsAndGotoAnalysisOrSpecificationStep:ProcessStep =
  {
    "DefineSCOsAndGotoAnalysisOrSpecificationStep"
  }
  end;

  obj ImplementStep:ProcessStep =
  {
    "Implement", ImplementationTool, ImplementationSubSteps, false
  }
  end;

  obj ImplementDataDesignStep:ProcessStep =
  {
    "ImplementDataDesignStep"
  }
  end;

  obj RefineModelClassDataRepresentationsStep:ProcessStep =
  {
    "RefineModelClassDataRepresentationsStep"
  }
  end;

  obj DefineNewInheritanceRelationshipsStep:ProcessStep =
  {
    "DefineNewInheritanceRelationshipsStep"
  }
  end;

  obj DesignAndImplementNewProcessClassesStep:ProcessStep =
  {
    "DesignAndImplementNewProcessClassesStep"
  }
  end;

  obj DefineAndImplementDataRepresentationClassesStep:ProcessStep =
  {
    "DefineAndImplementDataRepresentationClassesStep"
  }
  end;

  obj DesignAndImplementInterModuleSupportServicesStep:ProcessStep =
  {
    "DesignAndImplementInterModuleSupportServicesStep"
  }
  end;

  obj RegenerateDesignAndDataDiagramStep:ProcessStep =
  {
    "RegenerateDesignAndDataDiagramStep"
  }
  end;

  obj ImplementFunctionDesignStep:ProcessStep =
  {
    "ImplementFunctionDesignStep"
  }
  end;

  obj CodeFunctionBodiesStep:ProcessStep =
  {
    "CodeFunctionBodiesStep"
  }
  end;

  obj DefineNewProcessFunctionsStep:ProcessStep =
  {
    "DefineNewProcessFunctionsStep"
  }
  end;

  obj DefineProcessFunctionPreconditionAndPostconditionStep:ProcessStep =
  {
    "DefineProcessFunctionPreconditionAndPostconditionStep"
  }
  end;

  obj RefineFunctionCallingHierarchyStep:ProcessStep =
  {
    "RefineFunctionCallingHierarchyStep"
  }
  end;

  obj Use25LineRuleStep:ProcessStep =
  {
    "Use25LineRuleStep"
  }
  end;

  obj Use7PlusOrMin2FunctionCallRuleStep:ProcessStep =
  {
    "Use7PlusOrMin2FunctionCallRuleStep"
  }
  end;

  obj RegenerateDesignAndFunctionDiagramStep:ProcessStep =
  {
    "RegenerateDesignAndFunctionDiagramStep"
  }
  end;

  obj OptimizeImplementationStep:ProcessStep =
  {
    "OptimizeImplementationStep"
  }
  end;

  obj InlineFunctionsWhereAppropriateStep:ProcessStep =
  {
    "InlineFunctionsWhereAppropriateStep"
  }
  end;

  obj DefineMacrosWhereAppropriateStep:ProcessStep =
  {
    "DefineMacrosWhereAppropriateStep"
  }
  end;

  obj SubvertInformationHidingWhereAbsolutelyNecessaryForEfficiencyStep:ProcessStep =
  {
    "SubvertInformationHidingWhereAbsolutelyNecessaryForEfficiencyStep"
  }
  end;

  obj DefineSCOsAndGotoAnalysisOrSpecificationsStep:ProcessStep =
  {
    "DefineSCOsAndGotoAnalysisOrSpecificationsStep"
  }
  end;

  obj TestStep:ProcessStep = 
  {
    "Test", TestingTool, TestingSubSteps, false
  }
  end;

  obj PlanStep:ProcessStep =
  {
    "PlanStep"
  }
  end;

  obj PerformStep:ProcessStep =
  {
    "PerformStep"
  }
  end;

  obj WalkthroughStep:ProcessStep =
  {
    "WalkthroughStep"
  }
  end;

  obj FormallyReviewStep:ProcessStep =
  {
    "FormallyReviewStep"
  }
  end;

  obj ExecuteStep:ProcessStep =
  {
    "ExecuteStep"
  }
  end;

  obj ValidateStep:ProcessStep =
  {
    "ValidateStep"
  }
  end;

  obj FormallyVerifyStep:ProcessStep =
  {
    "FormallyVerifyStep"
  }
  end;

  obj ReportStep:ProcessStep =
  {
    "ReportStep"
  }
  end;

  obj DocumentStep:ProcessStep =
  {
    "Document", DocumentationTool, DocumentationSubSteps, false
  }
  end;

  obj ProduceFullUserDocumentationStep:ProcessStep =
  {
    "ProduceFullUserDocumentationStep"
  }
  end;

  obj ProduceFullSystemDocumentationStep:ProcessStep =
  {
    "ProduceFullSystemDocumentationStep"
  }
  end;

  obj ProduceSummaryDocumentViewsStep:ProcessStep =
  {
    "ProduceSummaryDocumentViewsStep"
  }
  end;

  obj ManageStep:ProcessStep =
  {
    "Manage", ManageTool, ManageSubSteps, false
  }
  end;

  obj ScheduleStep:ProcessStep =
  {
    "ScheduleStep"
  }
  end;

  obj CommunicateStep:ProcessStep =
  {
    "CommunicateStep"
  }
  end;

  op Expand
    inputs: ps:ProcessStep; 
    outputs: ps':ProcessSubSteps;
    pre:
       ps.pss != NULL;
    post:
        forall (ps:ProcessStep)
            (ps in ps') iff  (ps in ps.pss);

    description: (*
         When we want to get a subprocess from corrent process, the precondition is the current process
         and the subprocess must exist, the postcondition is the subprocess must show up after we click
         the subprocess name and the tool/expand.
    *);
    end Expand;

  op Collapse
    inputs: ps:ProcessSubStep;
    outputs: ps':ProcessStep;
    pre:
       ps.pss != NULL;
    post:
        forall (ps:ProcessSubSteps)
           (ps' in ps) iff (ps.pss in ps);
    description: (*
         When we want to from subprocess to go back to the previous process, we can choose the collapse, the
         precondition is the subprocess and previous process must exist, the postcondition is the precondition 
         must display after click the collapse.
    *);
    end Collapse;

(*  End of imported process.rsl materials  *)
(*******************************************)

(* Definition of objects derived from the above follows...these must also be global *)

 obj PassList is Pass* and NumPasses and CurrentPass
    description:  (*
	A PassList is the collection of all of the passes that make up the project,
	  plus indicators to the total number of passes and the current pass number.
    *);  
 end;

  obj Pass is Process
    description:  (*
	A Pass is a snapshot of the process, with settings corresponding to that pass.
    *);
 end;

  obj NumPasses is integer
    description:  (* 
	NumPasses is the current total of passes in the current project.
    *);
 end;

  obj CurrentPass is integer
    description:  (*
	CurrentPass is the current pass number.  Initialized to 0 in order to
		allow editing of pass 1 before it is engaged.
    *);
 end;

  obj SelectedCond is Pre or Post or Inv
    description:  (*
	Corresponds to the type of conditions (Pre, Post, Inv) chosen by
		the user on the Change Conditions screen.
	*);
  end;

  obj Pre;
  obj Post;
  obj Inv;

  op CreatePass(l:PassList)->(l':PassList)
    post:
	(* Creates a new Pass, which is added to the list with the existing Passes.
	 *  If user does not cancel, NumPasses is incremented to reflect added Pass.
	 *  The newly-created Pass is appended on to the end of the list.
	 *);
  end CreatePass;

  op DeletePass(l:PassList)->(l':PassList)
    pre:
	l.NumPasses !=0 and (l.CurrentPass != l.NumPasses);
    post:
	(* Deletes the highest numbered pass, as long as it is not the Current Pass.
	 *  If user does not cancel, NumPasses is decremented to reflect discarded Pass.
	 *)
	l' = l - l[NumPass];
  end DeletePass;

  op SelectCond(s:SelectedCond)->(s':SelectedCond)
    post:
	(* Operation to read the currently selected set of conditions to
		be changed *);
  end SelectCond;

  op Deactivate(p:ProcessStep,s:SelectedCond)->(p':ProcessStep)
    post:
	(* The selected conditions will not be enforced in this Pass *);
  end Deactivate;

  op Relax(p:ProcessStep,s:SelectedCond)->(p':ProcessStep)
    post:
	(* The selected conditions will not all be enforced in this Pass
*);
  end Relax;

  op Reactivate(p:ProcessStep,s:SelectedCond)->(p':ProcessStep)
    post:
	(* The selected conditions will be enforced in this Pass *);
  end Reactivate;

  op Strengthen(p:ProcessStep,s:SelectedCond)->(p':ProcessStep)
    post:
	(* Additional conditions will be enforced in this Pass *);
  end Strengthen;