From 07537c6d25bc34a2934df94db977dfe118676ddf Mon Sep 17 00:00:00 2001 From: monsterkrampe Date: Fri, 2 Sep 2022 15:03:07 +0200 Subject: [PATCH] Support more options and multiple models --- frontend/src/components/app.tsx | 94 ++++++++++++++++++++++++------- frontend/src/components/graph.tsx | 39 +++++++------ server/src/main.rs | 61 +++++++++++++------- 3 files changed, 138 insertions(+), 56 deletions(-) diff --git a/frontend/src/components/app.tsx b/frontend/src/components/app.tsx index 9661ca2..290baab 100644 --- a/frontend/src/components/app.tsx +++ b/frontend/src/components/app.tsx @@ -2,7 +2,21 @@ import * as React from 'react'; import { ThemeProvider, createTheme } from '@mui/material/styles'; import { - Backdrop, Button, CircularProgress, CssBaseline, Container, Link, Paper, Typography, TextField, + Backdrop, + Button, + CircularProgress, + CssBaseline, + Container, + FormControl, + FormControlLabel, + FormLabel, + Link, + Pagination, + Paper, + Radio, + RadioGroup, + Typography, + TextField, } from '@mui/material'; import Graph from './graph.tsx'; @@ -35,18 +49,27 @@ ac(10,and(neg(2),6)). ac(1,and(neg(7),2)). ac(6,neg(7)).ac(2,and(neg(9),neg(6))).`; +enum Parsing { + Naive = 'Naive', + Hybrid = 'Hybrid', +} + enum Strategy { ParseOnly = 'ParseOnly', Ground = 'Ground', - FirstComplete = 'FirstComplete', - FirstStable = 'FirstStable', - FirstStableNogood = 'FirstStableNogood', + Complete = 'Complete', + Stable = 'Stable', + StableCountingA = 'StableCountingA', + StableCountingB = 'StableCountingB', + StableNogood = 'StableNogood', } function App() { const [loading, setLoading] = useState(false); const [code, setCode] = useState(placeholder); - const [graph, setGraph] = useState(); + const [parsing, setParsing] = useState(Parsing.Naive); + const [graphs, setGraphs] = useState(); + const [graphIndex, setGraphIndex] = useState(0); const submitHandler = useCallback( (strategy: Strategy) => { @@ -57,18 +80,19 @@ function App() { headers: { 'Content-Type': 'application/json', }, - body: JSON.stringify({ code, strategy }), + body: JSON.stringify({ code, strategy, parsing }), }) .then((res) => res.json()) - .then((data) => setGraph(data)) + .then((data) => { + setGraphs(data); + setGraphIndex(0); + }) .finally(() => setLoading(false)); // TODO: error handling }, - [code], + [code, parsing], ); - console.log(graph); - return ( @@ -97,24 +121,56 @@ function App() { onChange={(event) => { setCode(event.target.value); }} /> - + + + Parsing Strategy + setParsing((e.target as HTMLInputElement).value)} + > + } label="Naive" /> + } label="Hybrid" /> + + +
+
{' '} {' '} - + {' '} - + {' '} - + + {' '} + + {' '} + - {graph + {graphs && ( - - - - + + {graphs.length > 1 + && ( + <> + Models: +
+ setGraphIndex(value - 1)} /> + + )} + {graphs.length > 0 + && ( + + + + )} + {graphs.length === 0 + && <>No models!} )} diff --git a/frontend/src/components/graph.tsx b/frontend/src/components/graph.tsx index 847a507..39a24c5 100644 --- a/frontend/src/components/graph.tsx +++ b/frontend/src/components/graph.tsx @@ -4,8 +4,6 @@ import G6 from '@antv/g6'; G6.registerNode('nodeWithFlag', { draw(cfg, group) { - console.log('cfg', cfg); - const mainWidth = Math.max(30, 5 * cfg.mainLabel.length + 10); const mainHeight = 30; @@ -14,10 +12,9 @@ G6.registerNode('nodeWithFlag', { width: mainWidth, height: mainHeight, radius: 2, - fill: cfg.fill || 'white', + fill: 'white', stroke: 'black', - lineWidth: cfg.lineWidth, - opacity: cfg.opacity, + cursor: 'pointer', }, name: 'rectMainLabel', draggable: true, @@ -32,6 +29,7 @@ G6.registerNode('nodeWithFlag', { text: cfg.mainLabel, fill: '#212121', fontFamily: 'Roboto', + cursor: 'pointer', }, // must be assigned in G6 3.3 and later versions. it can be any value you want name: 'textMailLabel', @@ -55,7 +53,7 @@ G6.registerNode('nodeWithFlag', { radius: 1, fill: '#4caf50', stroke: '#1b5e20', - opacity: cfg.opacity, + cursor: 'pointer', }, name: 'rectMainLabel', draggable: true, @@ -71,6 +69,7 @@ G6.registerNode('nodeWithFlag', { fill: '#212121', fontFamily: 'Roboto', fontSize: 10, + cursor: 'pointer', }, // must be assigned in G6 3.3 and later versions. it can be any value you want name: 'textMailLabel', @@ -97,29 +96,36 @@ G6.registerNode('nodeWithFlag', { // }, setState(name, value, item) { const group = item.getContainer(); - const shape = group.get('children')[0]; // Find the first graphics shape of the node. It is determined by the order of being added + const mainShape = group.get('children')[0]; // Find the first graphics shape of the node. It is determined by the order of being added + const subShape = group.get('children')[2]; if (name === 'hover') { if (value) { - shape.attr('fill', 'lightsteelblue'); + mainShape.attr('fill', 'lightsteelblue'); } else { - shape.attr('fill', 'white'); + mainShape.attr('fill', 'white'); } } if (name === 'highlight') { if (value) { - shape.attr('lineWidth', 3); + mainShape.attr('lineWidth', 3); } else { - shape.attr('lineWidth', 1); + mainShape.attr('lineWidth', 1); } } if (name === 'lowlight') { if (value) { - shape.attr('opacity', 0.3); + mainShape.attr('opacity', 0.3); + if (subShape) { + subShape.attr('opacity', 0.3); + } } else { - shape.attr('opacity', 1); + mainShape.attr('opacity', 1); + if (subShape) { + subShape.attr('opacity', 1); + } } } }, @@ -282,9 +288,6 @@ function Graph(props: Props) { .map(([source, target]) => `HI_${source}_${target}`), ); - console.log(relevantNodeIds); - console.log(relevantEdgeIds); - relevantNodeIds .forEach((id) => { graph.setItemState(id, 'lowlight', false); @@ -347,8 +350,8 @@ function Graph(props: Props) { return ( <>
-
- lo edge (condition is false) +
+ lo edge (condition is false) {' '} hi edge (condition is true)
diff --git a/server/src/main.rs b/server/src/main.rs index 4297469..557b154 100644 --- a/server/src/main.rs +++ b/server/src/main.rs @@ -8,20 +8,30 @@ use actix_cors::Cors; use actix_web::http; use adf_bdd::adf::{Adf, DoubleLabeledGraph}; +use adf_bdd::adfbiodivine::Adf as BdAdf; use adf_bdd::parser::AdfParser; +#[derive(Deserialize)] +enum Parsing { + Naive, + Hybrid, +} + #[derive(Deserialize)] enum Strategy { ParseOnly, Ground, - FirstComplete, - FirstStable, - FirstStableNogood, + Complete, + Stable, + StableCountingA, + StableCountingB, + StableNogood, } #[derive(Deserialize)] struct SolveReqBody { code: String, + parsing: Parsing, strategy: Strategy, } @@ -33,6 +43,7 @@ struct SolveResBody { #[post("/solve")] async fn solve(req_body: web::Json) -> impl Responder { let input = &req_body.code; + let parsing = &req_body.parsing; let strategy = &req_body.strategy; let parser = AdfParser::default(); @@ -43,29 +54,41 @@ async fn solve(req_body: web::Json) -> impl Responder { panic!("Parsing failed, see log for further details") } } - log::info!("[Done] parsing"); - let mut adf = Adf::from_parser(&parser); + let mut adf = match parsing { + Parsing::Naive => Adf::from_parser(&parser), + Parsing::Hybrid => { + let bd_adf = BdAdf::from_parser(&parser); + log::info!("[Start] translate into naive representation"); + let naive_adf = bd_adf.hybrid_step(); + log::info!("[Done] translate into naive representation"); + + naive_adf + } + }; log::debug!("{:?}", adf); - let ac = match strategy { - Strategy::ParseOnly => None, - Strategy::Ground => Some(adf.grounded()), - // TODO: error handling if no such model exists! - Strategy::FirstComplete => Some(adf.complete().next().unwrap()), - // TODO: error handling if no such model exists! - Strategy::FirstStable => Some(adf.stable().next().unwrap()), - // TODO: error handling if no such model exists! + let acs = match strategy { + Strategy::ParseOnly => vec![None], + Strategy::Ground => vec![Some(adf.grounded())], + Strategy::Complete => adf.complete().map(Some).collect(), + Strategy::Stable => adf.stable().map(Some).collect(), + // TODO: INPUT VALIDATION: only allow this for hybrid parsing + Strategy::StableCountingA => adf.stable_count_optimisation_heu_a().map(Some).collect(), + // TODO: INPUT VALIDATION: only allow this for hybrid parsing + Strategy::StableCountingB => adf.stable_count_optimisation_heu_b().map(Some).collect(), // TODO: support more than just default heuristics - Strategy::FirstStableNogood => Some( - adf.stable_nogood(adf_bdd::adf::heuristics::Heuristic::default()) - .next() - .unwrap(), - ), + Strategy::StableNogood => adf + .stable_nogood(adf_bdd::adf::heuristics::Heuristic::default()) + .map(Some) + .collect(), }; - let dto = adf.into_double_labeled_graph(ac.as_ref()); + let dto: Vec = acs + .iter() + .map(|ac| adf.into_double_labeled_graph(ac.as_ref())) + .collect(); web::Json(dto) }