001package conexp.fx.gui.exploration;
002
003import conexp.fx.core.algorithm.exploration.CounterExample;
004import conexp.fx.core.context.Implication;
005import conexp.fx.core.context.MatrixContext;
006import conexp.fx.core.util.IdGenerator;
007import conexp.fx.gui.ConExpFX;
008import conexp.fx.gui.dialog.ErrorDialog;
009import conexp.fx.gui.dialog.FXDialog;
010
011/*
012 * #%L
013 * Concept Explorer FX
014 * %%
015 * Copyright (C) 2010 - 2023 Francesco Kriegel
016 * %%
017 * This program is free software: you can redistribute it and/or modify
018 * it under the terms of the GNU General Public License as
019 * published by the Free Software Foundation, either version 3 of the
020 * License, or (at your option) any later version.
021 * 
022 * This program is distributed in the hope that it will be useful,
023 * but WITHOUT ANY WARRANTY; without even the implied warranty of
024 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
025 * GNU General Public License for more details.
026 * 
027 * You should have received a copy of the GNU General Public
028 * License along with this program.  If not, see
029 * <http://www.gnu.org/licenses/gpl-3.0.html>.
030 * #L%
031 */
032
033import javafx.beans.binding.Bindings;
034import javafx.beans.value.ObservableValue;
035import javafx.collections.FXCollections;
036import javafx.collections.ObservableList;
037import javafx.scene.Node;
038import javafx.scene.control.CheckBox;
039import javafx.scene.control.Label;
040import javafx.scene.control.TextField;
041import javafx.scene.layout.BorderPane;
042import javafx.scene.layout.HBox;
043import javafx.scene.layout.VBox;
044
045public class CounterExampleDialog extends FXDialog<CounterExample<String, String>> {
046
047  private final MatrixContext<String, String> context;
048  private final Implication<String, String>   implication;
049
050//  private final MatrixContext<String, String> counterExampleContext;
051
052  public CounterExampleDialog(
053      final MatrixContext<String, String> context,
054      final Implication<String, String> implication) {
055    super(
056        ConExpFX.instance.primaryStage,
057        Style.QUESTION,
058        "Attribute Exploration",
059        "Is the formal implication " + implication + " correct? If no, then please provide a counterexample.",
060        null);
061    this.context = context;
062    this.implication = implication;
063//    this.counterExampleContext =
064//        new MatrixContext<String, String>(
065//            SetLists.create("Counterexample" + IdGenerator.getNextId()),
066//            context.colHeads(),
067//            false);
068    this.setCenterNode(createCenterNode());
069  }
070
071  private final Node createCenterNode() {
072    final BorderPane pane = new BorderPane();
073//    final Text implicationText = new Text(implication.toString());
074//    implicationText.setWrappingWidth(300);
075//    implicationText.setFont(Font.font(12));
076//    pane.setTop(implicationText);
077
078    final Label objectLabel = new Label("Counterexample-Name: ");
079    final TextField objectTextField = new TextField("Counterexample" + IdGenerator.getNextId(context));
080    final HBox objectBox = new HBox(objectLabel, objectTextField);
081    final ObservableList<String> selectedAttributes = FXCollections.observableArrayList();
082    final ObservableValue<CounterExample<String, String>> counterExample = Bindings.createObjectBinding(
083        () -> new CounterExample<String, String>(objectTextField.getText(), selectedAttributes),
084        objectTextField.textProperty(),
085        selectedAttributes);
086    counterExample.addListener((__, ___, newValue) -> CounterExampleDialog.this.value = newValue);
087    selectedAttributes.addAll(implication.getPremise());
088    final VBox checkBoxes = new VBox();
089    for (String m : context.colHeads()) {
090      final CheckBox checkBox = new CheckBox(m);
091      if (implication.getPremise().contains(m)) {
092        checkBox.setSelected(true);
093        checkBox.setDisable(true);
094      } else {
095        checkBox.selectedProperty().addListener((__, ___, isSelected) -> {
096          if (isSelected)
097            selectedAttributes.add(checkBox.getText());
098          else
099            selectedAttributes.remove(checkBox.getText());
100        });
101      }
102      checkBoxes.getChildren().add(checkBox);
103    }
104    counterExample.addListener((__, ___, newValue) -> {
105      final boolean illegal = selectedAttributes.containsAll(implication.getPremise())
106          && selectedAttributes.containsAll(implication.getConclusion());
107      if (illegal) {
108        checkBoxes.getChildren().stream().map(child -> (CheckBox) child).forEach(
109            checkBox -> checkBox.setSelected(implication.getPremise().contains(checkBox.getText())));
110        new ErrorDialog(
111            ConExpFX.instance.primaryStage,
112            new IllegalArgumentException(
113                "An illegal counterexample was entered. The counterexample must not have all attributes in the implication's conclusion."))
114                    .showAndWait();
115      }
116    });
117    pane.setCenter(checkBoxes);
118    pane.setTop(objectBox);
119    return pane;
120//  pane.setMinWidth(600);
121//    final MatrixContextWidget<String, String> matrixContextWidget =
122//        new MatrixContextWidget<String, String>(null, false, counterExampleContext);
123//    matrixContextWidget.highlightToggleButton.setSelected(true);
124//    pane.setCenter(matrixContextWidget);
125//    pane.setMinHeight(500);
126//    pane.minHeightProperty().bind(
127//        new DoubleBinding() {
128//
129//          {
130//            bind(matrixContextWidget.height);
131//          }
132//
133//          @Override
134//          protected double computeValue() {
135////            System.out.println(matrixContextWidget.height.intValue());
136//            return matrixContextWidget.height.doubleValue() + implicationText.getBoundsInLocal().getHeight();
137//          }
138//        });
139//    counterExampleContext.addEventHandler(
140//        event -> {
141//          CounterExampleDialog.this.value = getCounterExample();
142//        },
143//        RelationEvent.ANY);
144  }
145
146//  private final CounterExample<String, String> getCounterExample() {
147//    final String object = counterExampleContext.rowHeads().get(
148//        0);
149//    final Set<String> attributes = counterExampleContext.row(object);
150//    return new CounterExample<String, String>(object, attributes);
151//  }
152
153}