1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-20 09:39:38 +01:00

Finish basic visualization of solve response

This commit is contained in:
monsterkrampe 2022-08-30 13:03:38 +02:00
parent 7c47d6aa28
commit b0e57cf7e1
No known key found for this signature in database
GPG Key ID: B8ADC1F5A5CE5057
2 changed files with 191 additions and 54 deletions

View File

@ -1,11 +1,13 @@
import * as React from 'react';
const { useState, useCallback } = React;
import { ThemeProvider, createTheme } from '@mui/material/styles';
import { Backdrop, Button, CircularProgress, CssBaseline, Container, Link, Typography, TextField } from '@mui/material';
import {
Backdrop, Button, CircularProgress, CssBaseline, Container, Link, Paper, Typography, TextField,
} from '@mui/material';
//import Graph from './graph.tsx';
import Graph from './graph.tsx';
const { useState, useCallback } = React;
const darkTheme = createTheme({
palette: {
@ -49,8 +51,8 @@ function App() {
},
body: JSON.stringify({ code }),
})
.then(res => res.json())
.then(data => setGraph(data))
.then((res) => res.json())
.then((data) => setGraph(data))
.finally(() => setLoading(false));
// TODO: error handling
},
@ -59,36 +61,53 @@ function App() {
console.log(graph);
return <ThemeProvider theme={darkTheme}>
<CssBaseline/>
<main>
<Typography variant="h2" component="h1" align="center" gutterBottom>
Solve your ADF Problem with Style!
</Typography>
return (
<ThemeProvider theme={darkTheme}>
<CssBaseline />
<main>
<Typography variant="h2" component="h1" align="center" gutterBottom>
Solve your ADF Problem with Style!
</Typography>
<Container>
<TextField
name="code"
label="Put your code here:"
helperText={<>For more info on the syntax, have a look <Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link>.</>}
multiline
fullWidth
variant="filled"
value={code}
onChange={(event) => { setCode(event.target.value); }}
/>
</Container>
<Container maxWidth="xs">
<Button fullWidth variant="outlined" onClick={submitHandler}>Solve it!</Button>
</Container>
</main>
<Container>
<TextField
name="code"
label="Put your code here:"
helperText={(
<>
For more info on the syntax, have a look
<Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link>
.
</>
)}
multiline
fullWidth
variant="filled"
value={code}
onChange={(event) => { setCode(event.target.value); }}
/>
</Container>
<Container maxWidth="xs">
<Button fullWidth variant="outlined" onClick={submitHandler}>Solve it!</Button>
</Container>
<Backdrop
open={loading}
>
<CircularProgress color="inherit" />
</Backdrop>
</ThemeProvider>;
{graph
&& (
<Container>
<Paper elevation={3} square sx={{ marginTop: 4, marginBottom: 4 }}>
<Graph graph={graph} />
</Paper>
</Container>
)}
</main>
<Backdrop
open={loading}
>
<CircularProgress color="inherit" />
</Backdrop>
</ThemeProvider>
);
}
export default App;

View File

@ -1,27 +1,50 @@
import React, { useEffect, useRef } from 'react';
import G6 from '@antv/g6';
import testData from '../test-data.ts';
function Graph() {
interface Props {
graph: {
lo_edges: [number, number][],
hi_edges: [number, number][],
node_labels: { [key: number]: string },
tree_root_labels: { [key: number]: string[] },
}
}
function Graph(props: Props) {
const { graph: graphProps } = props;
const ref = useRef(null);
let graph = null;
const graphRef = useRef();
useEffect(
() => {
if (!graph) {
graph = new G6.Graph({
if (!graphRef.current) {
graphRef.current = new G6.Graph({
container: ref.current,
width: 1200,
height: 800,
height: 600,
fitView: true,
rankdir: 'TB',
align: 'DR',
nodesep: 100,
ranksep: 100,
modes: {
default: ['drag-canvas', 'zoom-canvas', 'drag-node'],
},
layout: { type: 'dagre' },
defaultNode: {
anchorPoints: [[0.5, 0], [0, 0.5], [1, 0.5], [0.5, 1]],
type: 'rect',
style: {
r: 20,
radius: 2,
},
labelCfg: {
style: {
// fontWeight: 700,
fontFamily: 'Roboto',
},
},
},
defaultEdge: {
@ -49,6 +72,8 @@ function Graph() {
});
}
const graph = graphRef.current;
// Mouse enter a node
graph.on('node:mouseenter', (e) => {
const nodeItem = e.item; // Get the target item
@ -63,12 +88,31 @@ function Graph() {
// Click a node
graph.on('node:click', (e) => {
// Swich the 'click' state of the node to be false
const nodeItem = e.item; // et the clicked item
let onlyRemoveStates = false;
if (nodeItem.hasState('highlight')) {
onlyRemoveStates = true;
}
const clickNodes = graph.findAllByState('node', 'highlight');
clickNodes.forEach((cn) => {
graph.setItemState(cn, 'highlight', false);
});
const lowlightNodes = graph.findAllByState('node', 'lowlight');
lowlightNodes.forEach((cn) => {
graph.setItemState(cn, 'lowlight', false);
});
const lowlightEdges = graph.findAllByState('edge', 'lowlight');
lowlightEdges.forEach((cn) => {
graph.setItemState(cn, 'lowlight', false);
});
if (onlyRemoveStates) {
return;
}
graph.getNodes().forEach((node) => {
graph.setItemState(node, 'lowlight', true);
});
@ -76,24 +120,98 @@ function Graph() {
graph.setItemState(edge, 'lowlight', true);
});
const nodeItem = e.item; // et the clicked item
graph.setItemState(nodeItem, 'lowlight', false);
graph.setItemState(nodeItem, 'highlight', true);
nodeItem.getEdges().forEach((edge) => {
graph.setItemState(edge, 'lowlight', false);
});
});
const relevantNodeIds = [];
const relevantLoEdges = [];
const relevantHiEdges = [];
let newNodeIds = [nodeItem.getModel().id];
let newLoEdges = [];
let newHiEdges = [];
graph.data({
nodes: testData.map((node, index) => ({ id: index.toString(), label: node.label })),
edges: testData.flatMap((node, index) => [{ source: index.toString(), target: node.lo.toString(), style: { stroke: 'red', lineWidth: 2 } }, { source: index.toString(), target: node.hi.toString(), style: { stroke: 'green', lineWidth: 2 } }]),
while (newNodeIds.length > 0 || newLoEdges.length > 0 || newHiEdges.length > 0) {
relevantNodeIds.push(...newNodeIds);
relevantLoEdges.push(...newLoEdges);
relevantHiEdges.push(...newHiEdges);
newLoEdges = graphProps.lo_edges
.filter((edge) => relevantNodeIds.includes(edge[0].toString())
&& !relevantLoEdges.includes(edge));
newHiEdges = graphProps.hi_edges
.filter((edge) => relevantNodeIds.includes(edge[0].toString())
&& !relevantHiEdges.includes(edge));
newNodeIds = newLoEdges
.concat(newHiEdges)
.map((edge) => edge[1].toString())
.filter((id) => !relevantNodeIds.includes(id));
}
const relevantEdgeIds = relevantLoEdges
.map(([source, target]) => `LO_${source}_${target}`)
.concat(
relevantHiEdges
.map(([source, target]) => `HI_${source}_${target}`),
);
console.log(relevantNodeIds);
console.log(relevantEdgeIds);
relevantNodeIds
.forEach((id) => {
graph.setItemState(id, 'lowlight', false);
graph.setItemState(id, 'highlight', true);
});
relevantEdgeIds
.forEach((id) => {
graph.setItemState(id, 'lowlight', false);
});
// graph.setItemState(nodeItem, 'lowlight', false);
// graph.setItemState(nodeItem, 'highlight', true);
// nodeItem.getEdges().forEach((edge) => {
// graph.setItemState(edge, 'lowlight', false);
// });
});
graph.render();
},
[],
);
return <div ref={ref} />;
useEffect(
() => {
const graph = graphRef.current;
const nodes = Object.keys(graphProps.node_labels).map((id) => {
const mainLabel = graphProps.node_labels[id];
const subLabel = graphProps.tree_root_labels[id].length > 0 ? `Root for: ${graphProps.tree_root_labels[id].join(' ; ')}` : '';
const label = subLabel.length > 0 ? `${mainLabel}\n${subLabel}` : mainLabel;
return {
id: id.toString(),
label,
style: {
height: subLabel.length > 0 ? 60 : 30,
width: Math.max(30, 10 * mainLabel.length, 10 * subLabel.length),
},
};
});
const edges = graphProps.lo_edges.map(([source, target]) => ({
id: `LO_${source}_${target}`, source: source.toString(), target: target.toString(), style: { stroke: 'red', lineWidth: 2 },
}))
.concat(graphProps.hi_edges.map(([source, target]) => ({
id: `HI_${source}_${target}`, source: source.toString(), target: target.toString(), style: { stroke: 'green', lineWidth: 2 },
})));
graph.data({
nodes,
edges,
});
graph.render();
},
[graphProps],
);
return <div ref={ref} style={{ overflow: 'hidden' }} />;
}
export default Graph;