;HISTORY 1 Happens(AttCreateTP(TPDoneDeliverSellerBuyerCD45Exist),0). Happens(AttCreateTP(TPDonePayBuyerSeller167Exist),0). Happens(AttCreateTP(TPDoneBuyerExchMsgAgree23Exist),0). Happens(ExchMsg(Promise,Seller,Buyer,TPDoneDeliverSellerBuyerCD45Exist,TPDoneBuyerExchMsgAgree23Exist),1). Happens(ExchMsg1(Request,Seller,Buyer,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist,3),1). Happens(ExchMsg(Agree,Buyer,Seller,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist),2). Happens(Deliver(Seller,Buyer,CD),4). Happens(Pay(Buyer,Seller,1),6). >>> decreasoner.run('sviluppo/ACL.e') Discrete Event Calculus Reasoner 1.0 loading sviluppo/ACL.e loading foundations/Root.e loading foundations/EC.e 20320 variables and 71226 clauses relsat solver 1 model --- model 1: 0 Happens(AttCreateTP(TPDoneBuyerExchMsgAgree23Exist), 0). Happens(AttCreateTP(TPDoneDeliverSellerBuyerCD45Exist), 0). Happens(AttCreateTP(TPDonePayBuyerSeller167Exist), 0). Happens(Elapse(0), 0). 1 +ETP(TPDoneBuyerExchMsgAgree23Exist, Undef). +ETP(TPDoneDeliverSellerBuyerCD45Exist, Undef). +ETP(TPDonePayBuyerSeller167Exist, Undef). +TPDoneBuyerExchMsgAgree23Exist(). +TPDoneDeliverSellerBuyerCD45Exist(). +TPDonePayBuyerSeller167Exist(). Happens(AttCreateComm(Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist), 1). Happens(AttCreatePrecomm(Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3), 1). Happens(Elapse(1), 1). Happens(ExchMsg(Promise, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist), 1). Happens(ExchMsg1(Request, Seller, Buyer, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3), 1). 2 +Comm(Cond, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). +Precomm(Active, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3). Happens(AttAccceptPrecomm(Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist), 2). Happens(AttCreateComm(Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist), 2). Happens(Elapse(2), 2). Happens(ExchMsg(Agree, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist), 2). 3 -Comm(Cond, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). -ETP(TPDoneBuyerExchMsgAgree23Exist, Undef). -Precomm(Active, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3). +Comm(Cond, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). +Comm(Pending, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). +DoneBuyerExchMsgAgree(). +ETP(TPDoneBuyerExchMsgAgree23Exist, True). Happens(Elapse(3), 3). 4 Happens(Deliver(Seller, Buyer, CD), 4). Happens(Elapse(4), 4). 5 -Comm(Cond, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). -Comm(Pending, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). -ETP(TPDoneDeliverSellerBuyerCD45Exist, Undef). +Comm(Fulfilled, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). +Comm(Pending, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). +DoneDeliverSellerBuyerCD(). +ETP(TPDoneDeliverSellerBuyerCD45Exist, True). Happens(Elapse(5), 5). 6 Happens(Elapse(6), 6). Happens(Pay(Buyer, Seller, 1), 6). 7 -Comm(Pending, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). -ETP(TPDonePayBuyerSeller167Exist, Undef). +Comm(Fulfilled, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). +DonePayBuyerSeller1(). +ETP(TPDonePayBuyerSeller167Exist, True). Happens(Elapse(7), 7). 8 ACL: 0 predicates, 0 functions, 9 fluents, 10 events, 63 axioms EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms encoding 2438.6s/40.6m solution 6.6s total 2469.5s/41.2m ---------------------------------------------------------------------------------------- ;HISTORY 2 Happens(AttCreateTP(TPDoneDeliverSellerBuyerCD45Exist),0). Happens(AttCreateTP(TPDonePayBuyerSeller167Exist),0). Happens(AttCreateTP(TPDoneBuyerExchMsgAgree23Exist),0). Happens(ExchMsg(Promise,Seller,Buyer,TPDoneDeliverSellerBuyerCD45Exist,TPDoneBuyerExchMsgAgree23Exist),1). Happens(ExchMsg1(Request,Seller,Buyer,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist,3),1). Happens(ExchMsg(Agree,Buyer,Seller,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist),2). Happens(Deliver(Seller,Buyer,CD),4). Happens(Pay(Buyer,Seller,1),7). >>> decreasoner.run('sviluppo/ACL.e') Discrete Event Calculus Reasoner 1.0 loading sviluppo/ACL.e loading foundations/Root.e loading foundations/EC.e 20320 variables and 71226 clauses relsat solver 1 model --- model 1: 0 Happens(AttCreateTP(TPDoneBuyerExchMsgAgree23Exist), 0). Happens(AttCreateTP(TPDoneDeliverSellerBuyerCD45Exist), 0). Happens(AttCreateTP(TPDonePayBuyerSeller167Exist), 0). Happens(Elapse(0), 0). 1 +ETP(TPDoneBuyerExchMsgAgree23Exist, Undef). +ETP(TPDoneDeliverSellerBuyerCD45Exist, Undef). +ETP(TPDonePayBuyerSeller167Exist, Undef). +TPDoneBuyerExchMsgAgree23Exist(). +TPDoneDeliverSellerBuyerCD45Exist(). +TPDonePayBuyerSeller167Exist(). Happens(AttCreateComm(Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist), 1). Happens(AttCreatePrecomm(Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3), 1). Happens(Elapse(1), 1). Happens(ExchMsg(Promise, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist), 1). Happens(ExchMsg1(Request, Seller, Buyer, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3), 1). 2 +Comm(Cond, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). +Precomm(Active, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3). Happens(AttAccceptPrecomm(Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist), 2). Happens(AttCreateComm(Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist), 2). Happens(Elapse(2), 2). Happens(ExchMsg(Agree, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist), 2). 3 -Comm(Cond, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). -ETP(TPDoneBuyerExchMsgAgree23Exist, Undef). -Precomm(Active, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3). +Comm(Cond, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). +Comm(Pending, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). +DoneBuyerExchMsgAgree(). +ETP(TPDoneBuyerExchMsgAgree23Exist, True). Happens(Elapse(3), 3). 4 Happens(Deliver(Seller, Buyer, CD), 4). Happens(Elapse(4), 4). 5 -Comm(Cond, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). -Comm(Pending, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). -ETP(TPDoneDeliverSellerBuyerCD45Exist, Undef). +Comm(Fulfilled, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). +Comm(Pending, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). +DoneDeliverSellerBuyerCD(). +ETP(TPDoneDeliverSellerBuyerCD45Exist, True). Happens(Elapse(5), 5). 6 Happens(Elapse(6), 6). 7 Happens(Elapse(7), 7). Happens(Pay(Buyer, Seller, 1), 7). 8 -Comm(Pending, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). -ETP(TPDonePayBuyerSeller167Exist, Undef). +Comm(Violated, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist). +DonePayBuyerSeller1(). +ETP(TPDonePayBuyerSeller167Exist, False). ACL: 0 predicates, 0 functions, 9 fluents, 10 events, 63 axioms EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms encoding 2383.1s/39.7m solution 6.6s total 2415.6s/40.3m ------------------------------------------------------------------------ HISTORY 4 Happens(AttCreateTP(TPDoneDeliverSellerBuyerCD45Exist),0). Happens(AttCreateTP(TPDonePayBuyerSeller167Exist),0). Happens(AttCreateTP(TPDoneBuyerExchMsgAgree23Exist),0). Happens(ExchMsg(Promise,Seller,Buyer,TPDoneDeliverSellerBuyerCD45Exist,TPDoneBuyerExchMsgAgree23Exist),1). Happens(ExchMsg1(Request,Seller,Buyer,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist,3),1). ;no answer the parameter tout is crucial >>> decreasoner.run('sviluppo/ACL.e') Discrete Event Calculus Reasoner 1.0 loading sviluppo/ACL.e loading foundations/Root.e loading foundations/EC.e 20500 variables and 73206 clauses relsat solver 1 model --- model 1: 0 Happens(AttCreateTP(TPDoneBuyerExchMsgAgree23Exist), 0). Happens(AttCreateTP(TPDoneDeliverSellerBuyerCD45Exist), 0). Happens(AttCreateTP(TPDonePayBuyerSeller167Exist), 0). Happens(Elapse(0), 0). 1 +ETP(TPDoneBuyerExchMsgAgree23Exist, Undef). +ETP(TPDoneDeliverSellerBuyerCD45Exist, Undef). +ETP(TPDonePayBuyerSeller167Exist, Undef). +TPDoneBuyerExchMsgAgree23Exist(). +TPDoneDeliverSellerBuyerCD45Exist(). +TPDonePayBuyerSeller167Exist(). Happens(AttCreateComm(Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist), 1). Happens(AttCreatePrecomm(Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3), 1). Happens(Elapse(1), 1). Happens(ExchMsg(Promise, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist), 1). Happens(ExchMsg1(Request, Seller, Buyer, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3), 1). 2 +Comm(Cond, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). +Precomm(Active, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3). Happens(Elapse(2), 2). 3 Happens(Elapse(3), 3). 4 -Comm(Cond, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). -ETP(TPDoneBuyerExchMsgAgree23Exist, Undef). -Precomm(Active, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3). +Comm(Cancelled, Seller, Buyer, TPDoneDeliverSellerBuyerCD45Exist, TPDoneBuyerExchMsgAgree23Exist). +ETP(TPDoneBuyerExchMsgAgree23Exist, False). +Precomm(Cancelled, Buyer, Seller, TPDonePayBuyerSeller167Exist, TPDoneDeliverSellerBuyerCD45Exist, 3). Happens(Elapse(4), 4). 5 Happens(Elapse(5), 5). 6 -ETP(TPDoneDeliverSellerBuyerCD45Exist, Undef). +ETP(TPDoneDeliverSellerBuyerCD45Exist, False). Happens(Elapse(6), 6). 7 Happens(Elapse(7), 7). 8 -ETP(TPDonePayBuyerSeller167Exist, Undef). +ETP(TPDonePayBuyerSeller167Exist, False). ACL: 0 predicates, 0 functions, 9 fluents, 10 events, 60 axioms EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms encoding 2355.8s/39.3m solution 6.6s total 2384.3s/39.7m ------------------------------------------------------------------- HISTORY 5 Happens(AttCreateTP(TPDoneDeliverSellerBuyerCD45Exist),0). Happens(AttCreateTP(TPDonePayBuyerSeller167Exist),0). Happens(AttCreateTP(TPDoneBuyerExchMsgAgree23Exist),0). Happens(ExchMsg(Promise,Seller,Buyer,TPDoneDeliverSellerBuyerCD45Exist,TPDoneBuyerExchMsgAgree23Exist),1). Happens(ExchMsg1(Request,Seller,Buyer,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist,3),1). Happens(ExchMsg(Refuse,Buyer,Seller,TPDonePayBuyerSeller167Exist,TPDoneDeliverSellerBuyerCD45Exist),2).