Merge lp:~verifypn-wf/verifypn/petergame into lp:~verifypn-wf/verifypn/png

[Bogi]

[Bogi (boginw)]

review: Approve

Unmerged revisions

228. By Bogi on 2020-10-29

Added changes from Peter

=== modified file 'include/PetriEngine/AbstractPetriNetBuilder.h'
--- include/PetriEngine/AbstractPetriNetBuilder.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/AbstractPetriNetBuilder.h	2020-10-29 08:34:49 +0000
@@ -50,11 +50,14 @@
             exit(ErrorCode);
         }
         /** Add a new transition with a unique name */
-        virtual void addTransition(const std::string& name,
+        virtual void addTransition(
+                const std::string& name,
+                const uint32_t player,
                 double x = 0,
                 double y = 0) = 0;
         /** Add a new colored transition with a unique name */
         virtual void addTransition(const std::string& name,
+                const uint32_t player,
                 const Colored::GuardExpression_ptr& guard,
                 double x = 0,
                 double y = 0)
@@ -102,6 +105,8 @@
         virtual bool isColored() const {
             return _isColored;
         }
+        
+        virtual bool isGame() const = 0;
 
         virtual void sort() = 0;
         

=== modified file 'include/PetriEngine/Colored/ColoredNetStructures.h'
--- include/PetriEngine/Colored/ColoredNetStructures.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/Colored/ColoredNetStructures.h	2020-10-29 08:34:49 +0000
@@ -33,6 +33,7 @@
         struct Transition {
             std::string name;
             GuardExpression_ptr guard;
+            uint32_t player;
             std::vector<Arc> arcs;
         };
         

=== modified file 'include/PetriEngine/Colored/ColoredPetriNetBuilder.h'
--- include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2020-10-29 08:34:49 +0000
@@ -37,9 +37,11 @@
                 double x = 0,
                 double y = 0) override;
         void addTransition(const std::string& name,
+                const uint32_t player,
                 double x = 0,
                 double y = 0) override;
         void addTransition(const std::string& name,
+                const uint32_t player,
                 const Colored::GuardExpression_ptr& guard,
                 double x = 0,
                 double y = 0) override;
@@ -59,6 +61,7 @@
         void addColorType(const std::string& id,
                 Colored::ColorType* type) override;
 
+        bool isGame() const override;
 
         void sort() override;
 

=== modified file 'include/PetriEngine/NetStructures.h'
--- include/PetriEngine/NetStructures.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/NetStructures.h	2020-10-29 08:34:49 +0000
@@ -42,6 +42,7 @@
         std::vector<Arc> post;
         bool skip = false;
         bool inhib = false;
+        uint32_t player = 0;
         
         void addPreArc(const Arc& arc)
         {

=== modified file 'include/PetriEngine/PetriNet.h'
--- include/PetriEngine/PetriNet.h	2020-04-22 07:57:20 +0000
+++ include/PetriEngine/PetriNet.h	2020-10-29 08:34:49 +0000
@@ -59,6 +59,8 @@
     class PetriNet {
         PetriNet(uint32_t transitions, uint32_t invariants, uint32_t places);
     public:
+	typedef uint8_t player_t;
+
         ~PetriNet();
 
         uint32_t initial(size_t id) const;
@@ -68,6 +70,8 @@
         bool fireable(const MarkVal* marking, int transitionIndex);
         std::pair<const Invariant*, const Invariant*> preset(uint32_t id) const;
         std::pair<const Invariant*, const Invariant*> postset(uint32_t id) const;
+        bool ownedBy(uint32_t t, player_t p) const;
+        player_t owner(uint32_t t) const { return _players[t]; }
         uint32_t numberOfTransitions() const {
             return _ntransitions;
         }
@@ -103,6 +107,11 @@
         void sort();
         
         void toXML(std::ostream& out);
+    
+        static constexpr player_t NONE = 0;
+        static constexpr player_t CTRL = 1;
+        static constexpr player_t ENV = 2;
+        static constexpr player_t ANY = CTRL | ENV;
         
         const MarkVal* initial() const {
             return _initialMarking;
@@ -116,6 +125,8 @@
          */
         uint32_t _ninvariants, _ntransitions, _nplaces;
 
+        // transitions to players. To avoid overhead during normal verification.
+        std::vector<uint8_t> _players; // bool for now (ctrl==1, unctrl=2)
         std::vector<TransPtr> _transitions;
         std::vector<Invariant> _invariants;
         std::vector<uint32_t> _placeToPtrs;

=== modified file 'include/PetriEngine/PetriNetBuilder.h'
--- include/PetriEngine/PetriNetBuilder.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/PetriNetBuilder.h	2020-10-29 08:34:49 +0000
@@ -40,6 +40,7 @@
         PetriNetBuilder(const PetriNetBuilder& other);
         void addPlace(const std::string& name, int tokens, double x, double y) override;
         void addTransition(const std::string& name,
+                const uint32_t player,
                 double x,
                 double y) override;
         void addInputArc(const std::string& place,
@@ -49,6 +50,7 @@
         void addOutputArc(const std::string& transition, const std::string& place, int weight) override;
 
         virtual void sort() override;
+        virtual bool isGame() const;
         /** Make the resulting petri net, you take ownership */
         PetriNet* makePetriNet(bool reorder = true);
         /** Make the resulting initial marking, you take ownership */

=== modified file 'include/PetriEngine/SuccessorGenerator.h'
--- include/PetriEngine/SuccessorGenerator.h	2020-03-30 16:21:22 +0000
+++ include/PetriEngine/SuccessorGenerator.h	2020-10-29 08:34:49 +0000
@@ -21,11 +21,11 @@
 namespace PetriEngine {
 class SuccessorGenerator {
 public:
-    SuccessorGenerator(const PetriNet& net);
+    SuccessorGenerator(const PetriNet& net, bool is_game = false);
     SuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries);
     virtual ~SuccessorGenerator();
     void prepare(const Structures::State* state);
-    bool next(Structures::State& write);
+    bool next(Structures::State& write,  PetriNet::player_t player = PetriNet::ANY);
     uint32_t fired()
     {
         return _suc_tcounter -1;
@@ -65,6 +65,7 @@
     const Structures::State* _parent;
     uint32_t _suc_pcounter;
     uint32_t _suc_tcounter;
+    bool _is_game = false;
 
     friend class ReducingSuccessorGenerator;
 };

=== modified file 'include/PetriEngine/options.h'
--- include/PetriEngine/options.h	2020-04-04 14:48:55 +0000
+++ include/PetriEngine/options.h	2020-10-29 08:34:49 +0000
@@ -45,6 +45,8 @@
     bool isCPN = false;
     uint32_t seed_offset = 0;
 
+    // for game
+    bool isGame = false;
     void print() {
         if (!printstatistics) {
             return;

=== modified file 'include/PetriParse/PNMLParser.h'
--- include/PetriParse/PNMLParser.h	2020-03-02 21:03:24 +0000
+++ include/PetriParse/PNMLParser.h	2020-10-29 08:34:49 +0000
@@ -47,6 +47,7 @@
         std::string id;
         double x, y;
         PetriEngine::Colored::GuardExpression_ptr expr;
+        size_t player;
     };
     typedef std::vector<Transition> TransitionList;
     typedef TransitionList::iterator TransitionIter;

=== modified file 'src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp'
--- src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2020-03-02 21:03:24 +0000
+++ src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp	2020-10-29 08:34:49 +0000
@@ -33,19 +33,19 @@
         }
     }
 
-    void ColoredPetriNetBuilder::addTransition(const std::string& name, double x, double y) {
+    void ColoredPetriNetBuilder::addTransition(const std::string& name, const uint32_t player, double x, double y) {
         if (!_isColored) {
-            _ptBuilder.addTransition(name, x, y);
+            _ptBuilder.addTransition(name, player, x, y);
         }
     }
 
-    void ColoredPetriNetBuilder::addTransition(const std::string& name, const Colored::GuardExpression_ptr& guard, double x, double y) {
+    void ColoredPetriNetBuilder::addTransition(const std::string& name, const uint32_t player, const Colored::GuardExpression_ptr& guard, double x, double y) {
         if(_transitionnames.count(name) == 0)
         {
             uint32_t next = _transitionnames.size();
-            _transitions.emplace_back(Colored::Transition {name, guard});
+            _transitions.emplace_back(Colored::Transition {name, guard, player});
             _transitionnames[name] = next;
-        }
+        } else if (player != -1) _transitions[_transitionnames[name]].player = player;
     }
 
     void ColoredPetriNetBuilder::addInputArc(const std::string& place, const std::string& transition, bool inhibitor, int weight) {
@@ -72,7 +72,7 @@
         if(_transitionnames.count(transition) == 0)
         {
             std::cout << "Transition '" << transition << "' not found. Adding it." << std::endl;
-            addTransition(transition,0.0,0.0);
+            addTransition(transition,-1,0.0,0.0);
         }
         if(_placenames.count(place) == 0)
         {
@@ -97,7 +97,15 @@
     void ColoredPetriNetBuilder::addColorType(const std::string& id, Colored::ColorType* type) {
         _colors[id] = type;
     }
-
+    bool ColoredPetriNetBuilder::isGame() const {
+        for(size_t i = 0; i < _transitions.size(); ++i)
+        {
+            if(_transitions[i].player != 0)
+                return true;
+        }
+        return _ptBuilder.isGame();
+    }
+    
     void ColoredPetriNetBuilder::sort() {
 
     }
@@ -137,7 +145,7 @@
         size_t i = 0;
         for (auto& b : gen) {
             std::string name = transition.name + ";" + std::to_string(i++);
-            _ptBuilder.addTransition(name, 0.0, 0.0);
+            _ptBuilder.addTransition(name, transition.player, 0.0, 0.0);
             _pttransitionnames[transition.name].push_back(name);
             ++_npttransitions;
             for (auto& arc : transition.arcs) {
@@ -172,7 +180,7 @@
             }
 
             for (auto& transition : _transitions) {
-                _ptBuilder.addTransition(transition.name, 0.0, 0.0);
+                _ptBuilder.addTransition(transition.name, transition.player, 0.0, 0.0);
                 for (auto& arc : transition.arcs) {
                     try {
                         if (arc.input) {

=== modified file 'src/PetriEngine/PetriNet.cpp'
--- src/PetriEngine/PetriNet.cpp	2020-03-13 13:35:25 +0000
+++ src/PetriEngine/PetriNet.cpp	2020-10-29 08:34:49 +0000
@@ -33,6 +33,7 @@
 
     PetriNet::PetriNet(uint32_t trans, uint32_t invariants, uint32_t places)
     : _ninvariants(invariants), _ntransitions(trans), _nplaces(places),
+            _players(_ntransitions, 1),
             _transitions(_ntransitions+1),
             _invariants(_ninvariants),            
             _placeToPtrs(_nplaces+1) {
@@ -141,6 +142,12 @@
         uint32_t last = _transitions[id+1].inputs;
         return std::make_pair(&_invariants[first], &_invariants[last]);
     }
+
+    bool PetriNet::ownedBy(uint32_t id, player_t p) const {
+        if(p == ANY) return true;
+        return (p & _players[id]) != 0;
+    }
+
     
     bool PetriNet::fireable(const MarkVal *marking, int transitionIndex)
     {

=== modified file 'src/PetriEngine/PetriNetBuilder.cpp'
--- src/PetriEngine/PetriNetBuilder.cpp	2020-03-02 21:03:24 +0000
+++ src/PetriEngine/PetriNetBuilder.cpp	2020-10-29 08:34:49 +0000
@@ -59,20 +59,23 @@
         
     }
 
-    void PetriNetBuilder::addTransition(const string &name,
+    void PetriNetBuilder::addTransition(const string &name, const uint32_t player,
             double, double) {
         if(_transitionnames.count(name) == 0)
         {
             uint32_t next = _transitionnames.size();
             _transitions.emplace_back();
+            _transitions.back().player = player;
             _transitionnames[name] = next;
-        }
+        } 
+        else if(player != -1) 
+            _transitions[_transitionnames[name]].player = player;
     }
 
     void PetriNetBuilder::addInputArc(const string &place, const string &transition, bool inhibitor, int weight) {
         if(_transitionnames.count(transition) == 0)
         {
-            addTransition(transition,0.0,0.0);
+            addTransition(transition,-1,0.0,0.0);
         }
         if(_placenames.count(place) == 0)
         {
@@ -97,7 +100,7 @@
     void PetriNetBuilder::addOutputArc(const string &transition, const string &place, int weight) {
         if(_transitionnames.count(transition) == 0)
         {
-            addTransition(transition,0,0);
+            addTransition(transition,-1,0.0,0.0);
         }
         if(_placenames.count(place) == 0)
         {
@@ -309,6 +312,7 @@
                     --place_prod_count[post.place];
                     ++freeinv;
                 }
+                net->_players[freetrans] = (trans.player > 0) ? 2 : 1;
                 
                 trans_idmap[t] = freetrans;
                 
@@ -423,6 +427,15 @@
         
         return net;
     }
+
+    bool PetriNetBuilder::isGame() const {
+        for(size_t i = 0; i < _transitions.size(); ++i)
+        {
+            if(_transitions[i].player != 0)
+                return true;
+        }
+        return false;
+    }
     
     void PetriNetBuilder::sort()
     {

=== modified file 'src/PetriEngine/SuccessorGenerator.cpp'
--- src/PetriEngine/SuccessorGenerator.cpp	2020-03-02 21:03:24 +0000
+++ src/PetriEngine/SuccessorGenerator.cpp	2020-10-29 08:34:49 +0000
@@ -18,8 +18,8 @@
 #include <cassert>
 namespace PetriEngine {
 
-    SuccessorGenerator::SuccessorGenerator(const PetriNet& net)
-    : _net(net), _parent(NULL) {
+    SuccessorGenerator::SuccessorGenerator(const PetriNet& net, bool is_game)
+    : _net(net), _parent(NULL),  _is_game(is_game) {
         reset();
     }
     SuccessorGenerator::SuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries) : SuccessorGenerator(net){}
@@ -86,7 +86,7 @@
         }
     }
 
-    bool SuccessorGenerator::next(Structures::State& write) {
+    bool SuccessorGenerator::next(Structures::State& write, PetriNet::player_t player) {
         for (; _suc_pcounter < _net._nplaces; ++_suc_pcounter) {
             // orphans are currently under "place 0" as a special case
             if (_suc_pcounter == 0 || (*_parent).marking()[_suc_pcounter] > 0) {
@@ -95,7 +95,8 @@
                 }
                 uint32_t last = _net._placeToPtrs[_suc_pcounter + 1];
                 for (; _suc_tcounter != last; ++_suc_tcounter) {
-
+                    if (_is_game && !_net.ownedBy(_suc_tcounter, player))
+                        continue;
                     if (!checkPreset(_suc_tcounter)) continue;
                     memcpy(write.marking(), (*_parent).marking(), _net._nplaces * sizeof (MarkVal));
                     consumePreset(write, _suc_tcounter);
@@ -108,6 +109,7 @@
             }
             _suc_tcounter = std::numeric_limits<uint32_t>::max();
         }
+        reset();
         return false;
     }
 }

=== modified file 'src/PetriParse/PNMLParser.cpp'
--- src/PetriParse/PNMLParser.cpp	2020-03-10 14:09:07 +0000
+++ src/PetriParse/PNMLParser.cpp	2020-10-29 08:34:49 +0000
@@ -69,9 +69,9 @@
     //Add all the transition
     for (auto & transition : transitions)
         if (!isColored) {
-            builder->addTransition(transition.id, transition.x, transition.y);
+            builder->addTransition(transition.id, transition.player, transition.x, transition.y);
         } else {
-            builder->addTransition(transition.id, transition.expr, transition.x, transition.y);
+            builder->addTransition(transition.id, transition.player, transition.expr, transition.x, transition.y);
         }
 
     //Add all the arcs
@@ -553,6 +553,7 @@
     t.y = 0;
     t.id = element->first_attribute("id")->value();
     t.expr = nullptr;
+    t.player = 0;
 
 
     for (auto it = element->first_node(); it; it = it->next_sibling()) {
@@ -567,6 +568,12 @@
         } else if (strcmp(it->name(), "assignments") == 0) {
             std::cerr << "assignments not supported" << std::endl;
             exit(ErrorCode);
+        } 
+        else if (strcmp(it->name(), "player") == 0)
+        {
+            string text;
+            parseValue(it, text);
+            t.player = atoll(text.c_str());
         }
     }
     //Add transition to list

=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp	2020-04-28 20:13:40 +0000
+++ src/VerifyPN.cpp	2020-10-29 08:34:49 +0000
@@ -543,7 +543,8 @@
     PNMLParser parser;
     parser.parse(mfile, &builder);
     options.isCPN = builder.isColored();
-
+    options.isGame = builder.isGame();
+    
     // Close the file
     mfile.close();
     return ContinueCode;
@@ -686,6 +687,33 @@
         std::cerr << "CPN OverApproximation is only usable on colored models" << std::endl;
         return UnknownCode;
     }
+    if(options.isGame)
+    {
+        if(options.cpnOverApprox)
+        {
+            std::cerr << "CPN OverApproximation is not available for synthesis" << std::endl;
+            return UnknownCode;        
+        }
+        if(options.enablereduction != 0)
+        {
+            std::cerr << "Reductions are not available for synthesis" << std::endl;
+            return UnknownCode;
+        }
+        if(options.queryReductionTimeout != 0)
+        {
+            std::cerr << "Query-simplification is not available for synthesis" << std::endl;
+            return UnknownCode;
+        }
+        if(options.tar != 0)
+        {
+            std::cerr << "The TAR method does not support synthesis" << std::endl;
+            return UnknownCode;
+        }
+        if(options.stubbornreduction) {
+            std::cerr << "Stubborn reduction is not support for synthesis" << std::endl;
+            return UnknownCode;
+        }
+    }
     if (options.printstatistics) {
         std::cout << "Finished parsing model" << std::endl;
     }
@@ -824,6 +852,11 @@
 
                     if (options.queryReductionTimeout > 0 && qt > 0)
                     {
+                        if(options.isGame)
+                        {
+                            std::cerr << "Query-simplification is not available for synthesis" << std::endl;
+                            exit(UnknownCode);
+                        }
                         SimplificationContext simplificationContext(qm0, qnet.get(), qt,
                                 options.lpsolveTimeout, &cache);
                         try {
@@ -969,6 +1002,11 @@
         
     if (options.enablereduction > 0) {
         // Compute how many times each place appears in the query
+        if(options.isGame)
+        {
+            std::cerr << "Reductions are not available for synthesis" << std::endl;
+            return UnknownCode;
+        }
         builder.startTimer();
         builder.reduce(queries, results, options.enablereduction, options.trace, nullptr, options.reductionTimeout, options.reductions);
         printer.setReducer(builder.getReducer());        
@@ -998,6 +1036,11 @@
     }
     
     if (ctl_ids.size() > 0) {
+        if(options.gamemode)
+        {
+            std::cerr << "Synthesis-engine does not support CTL" << std::endl;
+            return UnknownCode;                    
+        }
         options.isctl=true;
         PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;
 
@@ -1060,6 +1103,11 @@
     
     if(options.tar && net->numberOfPlaces() > 0)
     {
+        if(options.isGame)
+        {
+            std::cerr << "The TAR method is not available for synthesis" << std::endl;
+            return UnknownCode;
+        }
         //Create reachability search strategy
         TARReachabilitySearch strategy(printer, *net, builder.getReducer(), options.kbound);
 
@@ -1074,6 +1122,11 @@
     }
     else
     {
+        if(options.gamemode)
+        {
+            std::cerr << "Synthesis-engine does not support Reachability" << std::endl;
+            return UnknownCode;                    
+        }
         ReachabilitySearch strategy(*net, printer, options.kbound);
 
         // Change default place-holder to default strategy