module cw/hypergraph
/*
   model based on definition in Rik Eshuis' thesis 

   is a model-in-progress - the constraints still need to be tightened
   I think

   dont know how to express constraints on Guards
     e.g. guards on hyperedges from a node with no triggers must be mutually exclusive and complete
   i.e something like:
   all n : Node | no n.trigger => True((HyperEdge$source.n).guard)
   all n : Node | all g1,g2 : (HyperEdge$source.n).guard | False(g1,g2)
   but I dont think I can write True and False in 1st order Alloy?

   Chris Wallace 11 Jan 2003
    rev 20 Jan 2003
*/

------------------------------------------------------------------------------------------
-- some generics
fun Injective[T,S] (r : T->S) {
     all t1,t2 : T | t1.r=t2.r => t1=t2
}

fun Surjective[T,S] (r : T-> S) {
     T.r = S
}
fun Bijective[T,S] (r : T-> S) {
     Injective(r) && Surjective(r)
}
-------------------------------------------------------------------------------------------
sig Activity { }

-----------------------------------------------------------------------------------------
sig Event { }

disj sig NamedEvent, ConditionChangeEvent, TerminationEvent, TemporalEvent extends Event { }
fact { Event in NamedEvent +  ConditionChangeEvent + TerminationEvent + TemporalEvent}

sig TerminationEvent1 extends TerminationEvent {
    term : ActivityNode
}


fact {TerminationEvent1 = TerminationEvent}
fact {TerminationEvent.TerminationEvent$term=ActivityNode}  -- cant use Surjection on subclass
fact {Injective(TerminationEvent$term) }


disj sig WhenEvent, AfterEvent extends TemporalEvent { }
fact { TemporalEvent in WhenEvent + AfterEvent}

disj sig NamedExternalEvent, NamedInternalEvent extends NamedEvent{}
fact {NamedEvent in NamedExternalEvent + NamedInternalEvent}

sig P2P, Broadcast extends Event{}

fact { all e : P2P |
         # HyperEdge$event.e =< 1
}

fact { all e : Broadcast |
         # HyperEdge$event.e  > 1
}

fact { TerminationEvent in P2P}
fact { AfterEvent in P2P }
fact { WhenEvent in Broadcast }
fact { NamedEvent in Broadcast}
fact { ConditionChangeEvent in Broadcast}
---------------------------------------------------------------------------------------
sig Node {  }

disj sig InitialNode, ActivityNode, WaitNode, FinalNode extends Node{ }

fact { Node in InitialNode + ActivityNode + WaitNode + FinalNode }

sig ActivityNode1 extends ActivityNode {
   act : Activity
}
fact {ActivityNode1 = ActivityNode}

fact {one InitialNode}

----------------------------------------------------------------------------------------
sig Guard { }
-----------------------------------------------------------------------------------------
sig HyperEdge {
  source : set Node,
  target : set Node,
  event : option Event,
  guard : option Guard,
  sendActions : set NamedInternalEvent 
}

fact {all h :HyperEdge | some h.source && some h.target }

fact { -- only Final nodes are never the source of hyperedges
    all n: Node | no HyperEdge$source.n => n in FinalNode
}

fact { -- only InitialNodes are never the target for hyperedges
    all n: Node | no HyperEdge$target.n => n in InitialNode
}

fact {Surjective(HyperEdge$event)}
fact {Surjective(HyperEdge$guard)}
fact {Surjective(ActivityNode$act)}

--------------------------------------------------------------------------------
fact c1 { -- if one of the sources of an hyperEdge is an ActivityNode
             -- it is the only source
   all h : HyperEdge |  all a : ActivityNode |
        a in h.source =>  h.source in a
}

fact c2 { -- every hyperedge which leaves an activity node is labelled
           -- with a corresponding activity termination event
   all h : HyperEdge | all a : ActivityNode |
        a in h.source => (h.event in TerminationEvent && h.event.term = a)
}

fact c3a { -- initial node can only be a source and if a source must be the 
          -- only one
   all h: HyperEdge |  InitialNode !in h.target && 
            ( InitialNode in h.source => h.source in InitialNode)
}

fact c3b { -- a final node can only be a target and if a target is final,
           -- so must all targets 
   all h: HyperEdge |  no (FinalNode & h.source) &&
            ( some FinalNode & h.target => h.target in FinalNode )
}

fact c4 { -- hyperedges leaving InitialNode must not have triggers
    all h : HyperEdge | h.source in InitialNode => no h.event
}

---------------------------------------------------------------------------------
sig Node1 extends Node {
    from, to : set Node
}
fact { Node1 = Node}

fact { all n : Node |  n.to = (HyperEdge$source.n).target }
fact { all n : Node |  n.from =(HyperEdge$target.n).source }

fact canStart { all n : Node - InitialNode | n in InitialNode.^to}
fact canFinish { all n : Node - FinalNode |  n in FinalNode.^from}

fact {some FinalNode }

fact noIdenticalHyperEdges{
    all h1,h2 : HyperEdge |
        h1.source = h2.source  &&
        h1.target = h2.target &&
        h1.event  = h2.event &&
        h1.guard  = h2.guard &&
        h1.sendActions = h2.sendActions 
		=> h1=h2
}


--------------------------------------------------------------------------------

fun show() {some HyperEdge && some ActivityNode && some WaitNode}

run show for 4