>>> decreasoner.run('sviluppo/auction.e') Discrete Event Calculus Reasoner 1.0 loading sviluppo/auction.e loading foundations/Root.e loading foundations/EC.e HISTORY Happens(AttCreateTP(TPDoneOpenAuction0145Exist),0). Happens(ExchMsgD(Declare,IntSystem,Bob,AssignRole(IntSystem,Bob,Auctioneer,Auction(01,Reg,4))),1). Happens(ExchMsgD(Declare,IntSystem,Carl,AssignRole(IntSystem,Carl,Participant,Auction(01,Reg,4))),1). Happens(ExchMsgD(Declare,IntSystem,Luke,AssignRole(IntSystem,Luke,Participant,Auction(01,Reg,4))),1). Happens(ExchMsgD(Declare,Bob,Carl,OpenAuction(01)),4). 74085 variables and 211367 clauses relsat solver 1 model --- model 1: 0 Happens(AttCreateTP(TPDoneOpenAuction0145Exist), 0). Happens(Elapse(0), 0). 1 +Auction(01, Reg, 4). +Context(AssignRole(IntSystem, Bob, Auctioneer, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Bob, Participant, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Carl, Auctioneer, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Carl, Participant, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Luke, Auctioneer, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Luke, Participant, Auction(01, Reg, 4))). +Context(OpenAuction(01)). +ETP(TPDoneOpenAuction0145Exist, Undef). +ETP(TPTrue, True). +Power(IntSystem, AssignRole(IntSystem, Bob, Auctioneer, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Bob, Participant, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Carl, Auctioneer, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Carl, Participant, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Luke, Auctioneer, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Luke, Participant, Auction(01, Reg, 4))). +RoleOf(Auctioneer, Auction(01, Reg, 4)). +RoleOf(Participant, Auction(01, Reg, 4)). +TPDoneOpenAuction0145Exist(). Happens(AssignRole(IntSystem, Bob, Auctioneer, Auction(01, Reg, 4)), 1). Happens(AssignRole(IntSystem, Carl, Participant, Auction(01, Reg, 4)), 1). Happens(AssignRole(IntSystem, Luke, Participant, Auction(01, Reg, 4)), 1). Happens(Elapse(1), 1). Happens(Empower(IntSystem, Bob, OpenAuction(01)), 1). Happens(ExchMsgD(Declare, IntSystem, Bob, AssignRole(IntSystem, Bob, Auctioneer, Auction(01, Reg, 4))), 1). Happens(ExchMsgD(Declare, IntSystem, Carl, AssignRole(IntSystem, Carl, Participant, Auction(01, Reg, 4))), 1). Happens(ExchMsgD(Declare, IntSystem, Luke, AssignRole(IntSystem, Luke, Participant, Auction(01, Reg, 4))), 1). 2 +HasRole(Bob, Auctioneer, Auction(01, Reg, 4)). +HasRole(Carl, Participant, Auction(01, Reg, 4)). +HasRole(Luke, Participant, Auction(01, Reg, 4)). +Norm(N1, Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, Elapse(3), TPDonePayBobAuctionHouse167Exist). +Power(Bob, OpenAuction(01)). Happens(Elapse(2), 2). 3 Happens(AttCreateComm(Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, SNorm, N1), 3). Happens(Elapse(3), 3). 4 +Comm(Pending, Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, SNorm, N1). Happens(Elapse(4), 4). Happens(ExchMsgD(Declare, Bob, Carl, OpenAuction(01)), 4). Happens(OpenAuction(01), 4). 5 -Auction(01, Reg, 4). -Comm(Pending, Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, SNorm, N1). -ETP(TPDoneOpenAuction0145Exist, Undef). +Auction(01, Open, 4). +Comm(Fulfilled, Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, SNorm, N1). +ETP(TPDoneOpenAuction0145Exist, True). EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms auction: 0 predicates, 0 functions, 11 fluents, 8 events, 36 axioms encoding 2799.1s/46.7m solution 34.9s total 2883.1s/48.1m ------------------------------------ Happens(AttCreateTP(TPDoneOpenAuction0145Exist),0). Happens(AttCreateTP(TPDonePayBobAuctionHouse167Exist),0). Happens(ExchMsgD(Declare,IntSystem,Bob,AssignRole(IntSystem,Bob,Auctioneer,Auction(01,Reg,4))),1). Happens(ExchMsgD(Declare,IntSystem,Carl,AssignRole(IntSystem,Carl,Participant,Auction(01,Reg,4))),1). Happens(ExchMsgD(Declare,IntSystem,Luke,AssignRole(IntSystem,Luke,Participant,Auction(01,Reg,4))),1). >>> decreasoner.run('sviluppo/04_Auction.e') Discrete Event Calculus Reasoner 1.0 loading sviluppo/04_Auction.e loading foundations/Root.e loading foundations/EC.e 168082 variables and 533654 clauses relsat solver 1 model --- model 1: 0 Happens(AttCreateTP(TPDoneOpenAuction0145Exist), 0). Happens(AttCreateTP(TPDonePayBobAuctionHouse167Exist), 0). Happens(Elapse(0), 0). 1 +Auction(01, Reg, 4). +Context(AssignRole(IntSystem, Bob, Auctioneer, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Bob, Participant, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Carl, Auctioneer, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Carl, Participant, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Luke, Auctioneer, Auction(01, Reg, 4))). +Context(AssignRole(IntSystem, Luke, Participant, Auction(01, Reg, 4))). +Context(OpenAuction(01)). +ETP(TPDoneOpenAuction0145Exist, Undef). +ETP(TPDonePayBobAuctionHouse167Exist, Undef). +ETP(TPTrue, True). +Power(IntSystem, AssignRole(IntSystem, Bob, Auctioneer, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Bob, Participant, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Carl, Auctioneer, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Carl, Participant, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Luke, Auctioneer, Auction(01, Reg, 4))). +Power(IntSystem, AssignRole(IntSystem, Luke, Participant, Auction(01, Reg, 4))). +RoleOf(Auctioneer, Auction(01, Reg, 4)). +RoleOf(Participant, Auction(01, Reg, 4)). +TPDoneOpenAuction0145Exist(). Happens(AssignRole(IntSystem, Bob, Auctioneer, Auction(01, Reg, 4)), 1). Happens(AssignRole(IntSystem, Carl, Participant, Auction(01, Reg, 4)), 1). Happens(AssignRole(IntSystem, Luke, Participant, Auction(01, Reg, 4)), 1). Happens(Elapse(1), 1). Happens(Empower(IntSystem, Bob, OpenAuction(01)), 1). Happens(ExchMsgD(Declare, IntSystem, Bob, AssignRole(IntSystem, Bob, Auctioneer, Auction(01, Reg, 4))), 1). Happens(ExchMsgD(Declare, IntSystem, Carl, AssignRole(IntSystem, Carl, Participant, Auction(01, Reg, 4))), 1). Happens(ExchMsgD(Declare, IntSystem, Luke, AssignRole(IntSystem, Luke, Participant, Auction(01, Reg, 4))), 1). 2 +HasRole(Bob, Auctioneer, Auction(01, Reg, 4)). +HasRole(Carl, Participant, Auction(01, Reg, 4)). +HasRole(Luke, Participant, Auction(01, Reg, 4)). +Norm(N1, Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, Elapse(3), TPDonePayBobAuctionHouse167Exist). +Power(Bob, OpenAuction(01)). Happens(Elapse(2), 2). 3 Happens(AttCreateComm(Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, SNorm, N1), 3). Happens(Elapse(3), 3). 4 +Comm(Pending, Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, SNorm, N1). Happens(Elapse(4), 4). 5 Happens(AttCreateComm(Bob, IntSystem, TPDonePayBobAuctionHouse167Exist, TPTrue, Sanction, N1), 5). Happens(Elapse(5), 5). 6 -Comm(Pending, Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, SNorm, N1). -ETP(TPDoneOpenAuction0145Exist, Undef). +Comm(Pending, Bob, IntSystem, TPDonePayBobAuctionHouse167Exist, TPTrue, Sanction, N1). +Comm(Violated, Bob, IntSystem, TPDoneOpenAuction0145Exist, TPTrue, SNorm, N1). +ETP(TPDoneOpenAuction0145Exist, False). Happens(Elapse(6), 6). 7 Happens(Elapse(7), 7). 8 -Comm(Pending, Bob, IntSystem, TPDonePayBobAuctionHouse167Exist, TPTrue, Sanction, N1). -ETP(TPDonePayBobAuctionHouse167Exist, Undef). +Comm(Violated, Bob, IntSystem, TPDonePayBobAuctionHouse167Exist, TPTrue, Sanction, N1). +ETP(TPDonePayBobAuctionHouse167Exist, False). 04_Auction: 0 predicates, 0 functions, 11 fluents, 8 events, 46 axioms EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms encoding 8416.4s/140.3m/2.3h solution 228.8s/3.8m total 8733.0s/145.5m/2.4h