|
@@ -15,155 +15,146 @@ All_RAM Control2EPN {
|
|
|
Post_Control_PW/Transition ct1 {
|
|
|
label = "0"
|
|
|
}
|
|
|
- Post_PetriNets_Runtime/Transition ct2 {
|
|
|
+ Post_Encapsulated_PetriNet/Transition ct2 {
|
|
|
label = "1"
|
|
|
- value_executing = $
|
|
|
- Boolean function value(model : Element, name : String, mapping : Element):
|
|
|
- return True!
|
|
|
- $
|
|
|
value_name = $
|
|
|
Integer function value(model : Element, name : String, mapping : Element):
|
|
|
return read_attribute(model, mapping["0"], "name")!
|
|
|
$
|
|
|
}
|
|
|
- Post_D2R_TransitionLink (ct1, ct2){
|
|
|
+ Post_C2P_TransitionLink (ct1, ct2){
|
|
|
label = "2"
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
- {Contains} ForAll copy_places {
|
|
|
+ {Contains} ForAll copy_states {
|
|
|
LHS {
|
|
|
- Pre_PetriNets/Place {
|
|
|
+ Pre_Control_PW/State {
|
|
|
label = "0"
|
|
|
}
|
|
|
}
|
|
|
RHS {
|
|
|
- Post_PetriNets/Place cp1 {
|
|
|
+ Post_Control_PW/State cp1 {
|
|
|
label = "0"
|
|
|
}
|
|
|
- Post_PetriNets_Runtime/Place cp2 {
|
|
|
+ Post_Encapsulated_PetriNet/Place cp2 {
|
|
|
label = "1"
|
|
|
value_tokens = $
|
|
|
Integer function value(model : Element, name : String, mapping : Element):
|
|
|
- return read_attribute(model, mapping["0"], "tokens")!
|
|
|
+ if (value_eq(read_attribute(model, mapping["0"], "initial"), True)):
|
|
|
+ return 1!
|
|
|
+ else:
|
|
|
+ return 0!
|
|
|
$
|
|
|
value_name = $
|
|
|
Integer function value(model : Element, name : String, mapping : Element):
|
|
|
return read_attribute(model, mapping["0"], "name")!
|
|
|
$
|
|
|
}
|
|
|
- Post_D2R_PlaceLink (cp1, cp2){
|
|
|
+ Post_C2P_PlaceLink (cp1, cp2){
|
|
|
label = "2"
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
{Contains} ForAll copy_P2T {
|
|
|
LHS {
|
|
|
- Pre_PetriNets/Place cp2t_p{
|
|
|
+ Pre_Control_PW/State cp2t_p{
|
|
|
label = "0"
|
|
|
}
|
|
|
- Pre_PetriNets/Transition cp2t_t{
|
|
|
+ Pre_Control_PW/Transition cp2t_t{
|
|
|
label = "1"
|
|
|
}
|
|
|
- Pre_PetriNets/P2T (cp2t_p, cp2t_t){
|
|
|
+ Pre_Control_PW/From (cp2t_p, cp2t_t){
|
|
|
label = "2"
|
|
|
}
|
|
|
- Pre_PetriNets_Runtime/Place cp2t_p2{
|
|
|
+ Pre_Encapsulated_PetriNet/Place cp2t_p2{
|
|
|
label = "3"
|
|
|
}
|
|
|
- Pre_PetriNets_Runtime/Transition cp2t_t2{
|
|
|
+ Pre_Encapsulated_PetriNet/Transition cp2t_t2{
|
|
|
label = "4"
|
|
|
}
|
|
|
- Pre_D2R_PlaceLink (cp2t_p, cp2t_p2){
|
|
|
+ Pre_C2P_PlaceLink (cp2t_p, cp2t_p2){
|
|
|
label = "5"
|
|
|
}
|
|
|
- Pre_D2R_TransitionLink (cp2t_t, cp2t_t2){
|
|
|
+ Pre_C2P_TransitionLink (cp2t_t, cp2t_t2){
|
|
|
label = "6"
|
|
|
}
|
|
|
}
|
|
|
RHS {
|
|
|
- Post_PetriNets/Place rhs_cp2t_p{
|
|
|
+ Post_Control_PW/State rhs_cp2t_p{
|
|
|
label = "0"
|
|
|
}
|
|
|
- Post_PetriNets/Transition rhs_cp2t_t{
|
|
|
+ Post_Control_PW/Transition rhs_cp2t_t{
|
|
|
label = "1"
|
|
|
}
|
|
|
- Post_PetriNets/P2T rhs_cp2t_p2t (rhs_cp2t_p, rhs_cp2t_t){
|
|
|
+ Post_Control_PW/P2T rhs_cp2t_p2t (rhs_cp2t_p, rhs_cp2t_t){
|
|
|
label = "2"
|
|
|
}
|
|
|
- Post_PetriNets_Runtime/Place rhs_cp2t_p2 {
|
|
|
+ Post_Encapsulated_PetriNet/Place rhs_cp2t_p2 {
|
|
|
label = "3"
|
|
|
}
|
|
|
- Post_PetriNets_Runtime/Transition rhs_cp2t_t2 {
|
|
|
+ Post_Encapsulated_PetriNet/Transition rhs_cp2t_t2 {
|
|
|
label = "4"
|
|
|
}
|
|
|
- Post_D2R_PlaceLink (rhs_cp2t_p, rhs_cp2t_p2){
|
|
|
+ Post_C2P_PlaceLink (rhs_cp2t_p, rhs_cp2t_p2){
|
|
|
label = "5"
|
|
|
}
|
|
|
- Post_D2R_TransitionLink (rhs_cp2t_t, rhs_cp2t_t2){
|
|
|
+ Post_C2P_TransitionLink (rhs_cp2t_t, rhs_cp2t_t2){
|
|
|
label = "6"
|
|
|
}
|
|
|
- Post_PetriNets_Runtime/P2T rhs_cp2t_p2t2(rhs_cp2t_p2, rhs_cp2t_t2) {
|
|
|
+ Post_Encapsulated_PetriNet/P2T rhs_cp2t_p2t2(rhs_cp2t_p2, rhs_cp2t_t2) {
|
|
|
label = "7"
|
|
|
- value_weight = $
|
|
|
- Integer function value(host_model : Element, name : String, mapping : Element):
|
|
|
- return read_attribute(host_model, mapping["2"], "weight")!
|
|
|
- $
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
{Contains} ForAll copy_T2P {
|
|
|
LHS {
|
|
|
- Pre_PetriNets/Place ct2p_p{
|
|
|
+ Pre_Control_PW/State ct2p_p{
|
|
|
label = "0"
|
|
|
}
|
|
|
- Pre_PetriNets/Transition ct2p_t{
|
|
|
+ Pre_Control_PW/Transition ct2p_t{
|
|
|
label = "1"
|
|
|
}
|
|
|
- Pre_PetriNets/T2P (ct2p_t, ct2p_p){
|
|
|
+ Pre_Control_PW/T2P (ct2p_t, ct2p_p){
|
|
|
label = "2"
|
|
|
}
|
|
|
- Pre_PetriNets_Runtime/Place ct2p_p2{
|
|
|
+ Pre_Encapsulated_PetriNet/Place ct2p_p2{
|
|
|
label = "3"
|
|
|
}
|
|
|
- Pre_PetriNets_Runtime/Transition ct2p_t2{
|
|
|
+ Pre_Encapsulated_PetriNet/Transition ct2p_t2{
|
|
|
label = "4"
|
|
|
}
|
|
|
- Pre_D2R_PlaceLink (ct2p_p, ct2p_p2){
|
|
|
+ Pre_C2P_PlaceLink (ct2p_p, ct2p_p2){
|
|
|
label = "5"
|
|
|
}
|
|
|
- Pre_D2R_TransitionLink (ct2p_t, ct2p_t2){
|
|
|
+ Pre_C2P_TransitionLink (ct2p_t, ct2p_t2){
|
|
|
label = "6"
|
|
|
}
|
|
|
}
|
|
|
RHS {
|
|
|
- Post_PetriNets/Place rhs_ct2p_p{
|
|
|
+ Post_Control_PW/Place rhs_ct2p_p{
|
|
|
label = "0"
|
|
|
}
|
|
|
- Post_PetriNets/Transition rhs_ct2p_t{
|
|
|
+ Post_Control_PW/Transition rhs_ct2p_t{
|
|
|
label = "1"
|
|
|
}
|
|
|
- Post_PetriNets/T2P (rhs_ct2p_t, rhs_ct2p_p){
|
|
|
+ Post_Control_PW/T2P (rhs_ct2p_t, rhs_ct2p_p){
|
|
|
label = "2"
|
|
|
}
|
|
|
- Post_PetriNets_Runtime/Place rhs_ct2p_p2 {
|
|
|
+ Post_Encapsulated_PetriNet/Place rhs_ct2p_p2 {
|
|
|
label = "3"
|
|
|
}
|
|
|
- Post_PetriNets_Runtime/Transition rhs_ct2p_t2 {
|
|
|
+ Post_Encapsulated_PetriNet/Transition rhs_ct2p_t2 {
|
|
|
label = "4"
|
|
|
}
|
|
|
- Post_D2R_PlaceLink (rhs_ct2p_p, rhs_ct2p_p2){
|
|
|
+ Post_C2P_PlaceLink (rhs_ct2p_p, rhs_ct2p_p2){
|
|
|
label = "5"
|
|
|
}
|
|
|
- Post_D2R_TransitionLink (rhs_ct2p_t, rhs_ct2p_t2){
|
|
|
+ Post_C2P_TransitionLink (rhs_ct2p_t, rhs_ct2p_t2){
|
|
|
label = "6"
|
|
|
}
|
|
|
- Post_PetriNets_Runtime/T2P (rhs_ct2p_t2, rhs_ct2p_p2) {
|
|
|
+ Post_Encapsulated_PetriNet/T2P (rhs_ct2p_t2, rhs_ct2p_p2) {
|
|
|
label = "7"
|
|
|
- value_weight = $
|
|
|
- Integer function value(host_model : Element, name : String, mapping : Element):
|
|
|
- return read_attribute(host_model, mapping["2"], "weight")!
|
|
|
- $
|
|
|
}
|
|
|
}
|
|
|
}
|