← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/PQL/Expressions.cpp

  • Committer: Simon Virenfeldt
  • Date: 2020-12-21 12:13:16 UTC
  • mfrom: (240.1.1 ltl_model_checker)
  • Revision ID: simwir1@gmail.com-20201221121316-adtl6y7g44vhxo8z
Merge ltl-xml-write@241

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/PetriEngine/PQL/Expressions.cpp
1649
1649
            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
1650
1650
            _cond->toBinary(out);
1651
1651
        }
1652
 
        
 
1652
 
1653
1653
        void UntilCondition::toBinary(std::ostream& out) const
1654
1654
        {
1655
1655
            auto path = getPath();
1860
1860
            _cond2->toXML(out,tabs+3);
1861
1861
            generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
1862
1862
        }
1863
 
        
 
1863
 
 
1864
        void ACondition::toXML(std::ostream& out, uint32_t tabs) const {
 
1865
            generateTabs(out, tabs) << "<all-paths>\n";
 
1866
            _cond->toXML(out, tabs+1);
 
1867
            generateTabs(out, tabs) << "</all-paths>\n";
 
1868
        }
 
1869
 
 
1870
        void ECondition::toXML(std::ostream& out, uint32_t tabs) const {
 
1871
            generateTabs(out, tabs) << "<exists-path>\n";
 
1872
            _cond->toXML(out, tabs+1);
 
1873
            generateTabs(out, tabs) << "</exists-path>\n";
 
1874
        }
 
1875
 
 
1876
        void FCondition::toXML(std::ostream& out, uint32_t tabs) const {
 
1877
            generateTabs(out, tabs) << "<finally>\n";
 
1878
            _cond->toXML(out, tabs+1);
 
1879
            generateTabs(out, tabs) << "</finally>\n";
 
1880
        }
 
1881
 
 
1882
        void GCondition::toXML(std::ostream& out, uint32_t tabs) const {
 
1883
            generateTabs(out, tabs) << "<globally>\n";
 
1884
            _cond->toXML(out, tabs+1);
 
1885
            generateTabs(out, tabs) << "</globally>\n";
 
1886
        }
 
1887
 
 
1888
        void XCondition::toXML(std::ostream& out, uint32_t tabs) const {
 
1889
            generateTabs(out, tabs) << "<next>\n";
 
1890
            _cond->toXML(out, tabs+1);
 
1891
            generateTabs(out, tabs) << "</next>\n";
 
1892
        }
 
1893
 
 
1894
        void UntilCondition::toXML(std::ostream& out, uint32_t tabs) const {
 
1895
            generateTabs(out,tabs) << "<until>\n" ; generateTabs(out,tabs+1) << "<before>\n";
 
1896
            _cond1->toXML(out,tabs+2);
 
1897
            generateTabs(out,tabs+1) << "</before>\n" ; generateTabs(out,tabs+1) << "<reach>\n";
 
1898
            _cond2->toXML(out,tabs+2);
 
1899
            generateTabs(out,tabs+1) << "</reach>\n" ; generateTabs(out,tabs) << "</until>\n" ;
 
1900
        }
 
1901
 
 
1902
 
 
1903
 
1864
1904
        void AndCondition::toXML(std::ostream& out,uint32_t tabs) const {
1865
1905
            if(_conds.size() == 0)
1866
1906
            {
3525
3565
            return ECondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);
3526
3566
        }
3527
3567
 
 
3568
 
3528
3569
        Condition_ptr ECondition::pushNegation(negstat_t &stats, const EvaluationContext &context, bool nested, bool negated,
3529
3570
                                               bool initrw) {
3530
3571
            assert(false);