File

src/app/dialogs/result-tree/result-tree.dialog.ts

Index

Properties

Properties

expandable
expandable: boolean
Type : boolean
level
level: number
Type : number
trace
trace: ModelCheckerTrace
Type : ModelCheckerTrace
visible
visible: boolean
Type : boolean
import { FlatTreeControl } from '@angular/cdk/tree';
import { Component, Inject, OnInit } from '@angular/core';
import { MAT_LEGACY_DIALOG_DATA as MAT_DIALOG_DATA, MatLegacyDialogRef as MatDialogRef } from '@angular/material/legacy-dialog';
import { MatTreeFlatDataSource, MatTreeFlattener } from '@angular/material/tree';

import { ModelCheckerResponse } from 'src/app/model/api/model-checker-response';
import { ModelCheckerTrace } from 'src/app/model/api/model-checker-trace';
import { SnackBarService } from 'src/app/services/snack-bar.service';

interface FlatTraceNode {
  trace: ModelCheckerTrace;
  expandable: boolean;
  visible: boolean;
  level: number;
}

/**
 * Dialog that shows the result of a ModelChecking request in a tree-structure.
 * Provides options to control the tree, depending on the feedback level.
 */
@Component({
  templateUrl: './result-tree.dialog.html',
  styleUrls: ['./result-tree.dialog.scss'],
})
export class ResultTreeDialog implements OnInit {
  public readonly treeControl = new FlatTreeControl<FlatTraceNode>(
    (node) => node.level,
    (node) => node.expandable,
  );

  public readonly dataSource = new MatTreeFlatDataSource(
    this.treeControl,
    new MatTreeFlattener(
      traceToFlatNode,
      (node) => node.level,
      (node) => node.expandable,
      (node) => node.children,
    ),
  );

  public constructor(
    private readonly dialogRef: MatDialogRef<ResultTreeDialog>,
    @Inject(MAT_DIALOG_DATA) public readonly result: ModelCheckerResponse,
    private readonly snackBarService: SnackBarService,
  ) {}

  public ngOnInit(): void {
    this.dataSource.data = [this.result.rootTrace];
    if (this.result.feedback === 'relevant') {
      this.expandAll();
    }
  }

  public closeDialog(): void {
    this.dialogRef.close();
  }

  public hasChild(_: number, node: FlatTraceNode): boolean {
    return node.expandable;
  }

  public expandAll(): void {
    try {
      this.treeControl.expandAll();
    } catch (_) {
      this.snackBarService.openSnackBar({ key: 'result-tree.expand-error' });
    }
  }

  public updateFilter(filter: boolean): void {
    if (!filter) {
      // Set all nodes to visible.
      this.treeControl.dataNodes.forEach((node) => (node.visible = true));
    } else {
      // Recursively, set irrelevant nodes to invisible.
      this.filterCauses(this.treeControl.dataNodes[0], this.result.rootTrace.isModel, true);
    }
  }

  private filterCauses(node: FlatTraceNode, expected: boolean, parentIsVisible: boolean): void {
    // Check if trace behaved as required.
    const actual = node.trace.isModel === node.trace.shouldBeModel;
    // Check if filtering is for positive or negative causes
    const visible = parentIsVisible && actual === expected;
    node.visible = visible;
    // Currently, there's no method to retrieve immediate children for the FlatTreeControl.
    // As a workaround, we get all descendants and filter them by their level.
    this.treeControl.getDescendants(node).forEach((child) => {
      if (child.level === node.level + 1) {
        this.filterCauses(child, expected, visible);
      }
    });
  }
}

function traceToFlatNode(trace: ModelCheckerTrace, level: number): FlatTraceNode {
  return {
    trace,
    expandable: !!trace.children && trace.children.length > 0,
    visible: true,
    level,
  };
}

results matching ""

    No results matching ""