/* Copyright (C) 2013-2021 TU Dortmund
 * This file is part of AutomataLib, http://www.automatalib.net/.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package net.automatalib.examples.modelchecking;

import java.util.function.Function;

import net.automatalib.automata.spa.CFMPSView;
import net.automatalib.automata.spa.SPA;
import net.automatalib.examples.spa.PalindromeExample;
import net.automatalib.graphs.ContextFreeModalProcessSystem;
import net.automatalib.modelcheckers.m3c.formula.FormulaNode;
import net.automatalib.modelcheckers.m3c.formula.parser.M3CParser;
import net.automatalib.modelcheckers.m3c.formula.parser.ParseException;
import net.automatalib.modelcheckers.m3c.solver.M3CSolver;
import net.automatalib.modelcheckers.m3c.solver.M3CSolver.TypedM3CSolver;
import net.automatalib.modelcheckers.m3c.solver.M3CSolvers;
import net.automatalib.visualization.Visualization;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * An example in which we transform the {@link PalindromeExample palindrome SPA} into a {@link
 * ContextFreeModalProcessSystem} and use the {@link M3CSolver} to evaluate properties on the system.
 *
 * @author frohme
 */
public final class M3CSPAExample {

    private static final Logger LOGGER = LoggerFactory.getLogger(M3CSPAExample.class);

    private M3CSPAExample() {
        // prevent initialization
    }

    public static void main(String[] args) throws ParseException {
        final SPA<?, Character> spa = PalindromeExample.buildSPA();
        final CFMPSView<Character> view = new CFMPSView<>(spa);

        //@formatter:off
        final String[] formulas = {"mu X.(<>X || <b><b>true)", // there exists a path with "bb"
                                   "mu X.(<>X || <b><S><b>true)", // there exists a path with "bSb"
                                   "mu X.(<>X || <b><T><b>true)", // there exists a path with "bTb"
                                   "<S><T><a>true", // There exists a starting sequence of STa
                                   "<S><T><b>true", // There exists a starting sequence of STb
                                   "<S><T><c>true", // There exists a starting sequence of STc
                                   "<S><a><T><c>true", // There exists a starting sequence of SaTc
                                   "<S><a><S><T><c>true", // There exists a starting sequence of SaSTc
                                   "nu X. ([]X && [] false)", // all paths reach the final state
                                   "mu X. (<>X || [] false)", // there exists a path to the final state
                                   "nu X. ([]X && mu Y. (<>Y || [] false))", // on all paths there exists a path to the final state
                                   "nu X. ([]X && (<S>true -> [S](mu Y. (<>Y || <R>true))))", // globally, if there exists an S, it must be followed by an R eventually
        };
        //@formatter:on

        final Function<String, Character> labelParser = s -> s.charAt(0);
        final Function<String, Void> apParser = s -> null;
        final TypedM3CSolver<FormulaNode<Character, Void>> solver = M3CSolvers.typedSolver(view);

        for (String f : formulas) {
            final FormulaNode<Character, Void> formula = M3CParser.parse(f, labelParser, apParser);
            LOGGER.info("Is '{}' satisfied? {}", f, solver.solve(formula));
        }

        Visualization.visualize(view);
    }
}

@@ -2136,28 +2136,18 @@
 las = %7B%22
-mu X.(%3C%3EX %7C%7C
+EF
  %3Cb%3E%3Cb%3Et
@@ -2141,33 +2141,32 @@
  %7B%22EF %3Cb%3E%3Cb%3Etrue
-)
 %22, // there exis
@@ -2217,36 +2217,26 @@
            %22
-mu X.(%3C%3EX %7C%7C
+EF
  %3Cb%3E%3CS%3E%3Cb%3Etr
@@ -2229,33 +2229,32 @@
 EF %3Cb%3E%3CS%3E%3Cb%3Etrue
-)
 %22, // there exis
@@ -2314,20 +2314,10 @@
    %22
-mu X.(%3C%3EX %7C%7C
+EF
  %3Cb%3E
@@ -2326,17 +2326,16 @@
 %3E%3Cb%3Etrue
-)
 %22, // th
@@ -2886,29 +2886,18 @@
        %22
-nu X. (%5B%5DX &&
+EF
  %5B%5D fals
@@ -2901,30 +2901,36 @@
 alse
-)
 %22, // 
-all paths reach
+there exists a path to
  the
@@ -2982,21 +2982,10 @@
    %22
-mu X. (%3C%3EX %7C%7C
+AF
  %5B%5D 
@@ -2993,37 +2993,29 @@
 alse
-)
 %22, // 
-there exists a path to
+all paths reach
  the
@@ -3067,35 +3067,13 @@
    %22
-nu X. (%5B%5DX && mu Y. (%3C%3EY %7C%7C
+AG EF
  %5B%5D 
@@ -3077,18 +3077,16 @@
 %5B%5D false
-))
 %22, // on
@@ -3175,51 +3175,19 @@
    %22
-nu X. (%5B%5DX && (%3CS%3Etrue -%3E %5BS%5D(mu Y. (%3C%3EY %7C%7C
+AG (%5BS%5D (AF
  %3CR%3E
@@ -3192,18 +3192,16 @@
 R%3Etrue))
-))
 %22, // gl
@@ -3212,32 +3212,20 @@
 ly, 
-if there exists an S, it
+every S path
  mus

rewrite SPA formulae in CTL