Support more options and multiple models

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',
+  Complete = 'Complete',
-  FirstStable = 'FirstStable',
+  Stable = 'Stable',
-  FirstStableNogood = 'FirstStableNogood',
+  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 (
     <ThemeProvider theme={darkTheme}>
       <CssBaseline />
@@ -97,24 +121,56 @@ function App() {
             onChange={(event) => { setCode(event.target.value); }}
           />
         </Container>
-        <Container>
+        <Container sx={{ marginTop: 2, marginBottom: 2 }}>
+          <FormControl>
+            <FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
+            <RadioGroup
+              row
+              aria-labelledby="parsing-radio-group"
+              name="parsing"
+              value={parsing}
+              onChange={(e) => setParsing((e.target as HTMLInputElement).value)}
+            >
+              <FormControlLabel value={Parsing.Naive} control={<Radio />} label="Naive" />
+              <FormControlLabel value={Parsing.Hybrid} control={<Radio />} label="Hybrid" />
+            </RadioGroup>
+          </FormControl>
+          <br />
+          <br />
           <Button variant="outlined" onClick={() => submitHandler(Strategy.ParseOnly)}>Parse only</Button>
           {' '}
           <Button variant="outlined" onClick={() => submitHandler(Strategy.Ground)}>Grounded Model</Button>
           {' '}
-          <Button variant="outlined" onClick={() => submitHandler(Strategy.FirstComplete)}>(First) Complete Model</Button>
+          <Button variant="outlined" onClick={() => submitHandler(Strategy.Complete)}>Complete Models</Button>
           {' '}
-          <Button variant="outlined" onClick={() => submitHandler(Strategy.FirstStable)}>(First) Stable Model</Button>
+          <Button variant="outlined" onClick={() => submitHandler(Strategy.Stable)}>Stable Models (naive heuristics)</Button>
           {' '}
-          <Button variant="outlined" onClick={() => submitHandler(Strategy.FirstStableNogood)}>(First) Stable Model using nogoods</Button>
+          <Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingA)}>Stable Models (counting heuristic A)</Button>
+          {' '}
+          <Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingB)}>Stable Models (counting heuristic B)</Button>
+          {' '}
+          <Button variant="outlined" onClick={() => submitHandler(Strategy.StableNogood)}>Stable Models using nogoods (Simple Heuristic)</Button>
         </Container>
 
-        {graph
+        {graphs
         && (
-        <Container>
+        <Container sx={{ marginTop: 4, marginBottom: 4 }}>
-          <Paper elevation={3} square sx={{ marginTop: 4, marginBottom: 4 }}>
+          {graphs.length > 1
-            <Graph graph={graph} />
+            && (
-          </Paper>
+            <>
+              Models:
+              <br />
+              <Pagination variant="outlined" shape="rounded" count={graphs.length} page={graphIndex + 1} onChange={(e, value) => setGraphIndex(value - 1)} />
+            </>
+            )}
+          {graphs.length > 0
+            && (
+            <Paper elevation={3} square sx={{ marginTop: 4, marginBottom: 4 }}>
+              <Graph graph={graphs[graphIndex]} />
+            </Paper>
+            )}
+          {graphs.length === 0
+            && <>No models!</>}
         </Container>
         )}
       </main>

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,
+        cursor: 'pointer',
-        opacity: cfg.opacity,
       },
       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 (
     <>
       <div ref={ref} style={{ overflow: 'hidden' }} />
-      <div>
+      <div style={{ padding: 4 }}>
-        <span style={{ color: '#ed6c02' }}>lo edge (condition is false)</span>
+        <span style={{ color: '#ed6c02', marginRight: 8 }}>lo edge (condition is false)</span>
         {' '}
         <span style={{ color: '#1976d2' }}>hi edge (condition is true)</span>
       </div>

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,
+    Complete,
-    FirstStable,
+    Stable,
-    FirstStableNogood,
+    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<SolveReqBody>) -> 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<SolveReqBody>) -> 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 {
+    let acs = match strategy {
-        Strategy::ParseOnly => None,
+        Strategy::ParseOnly => vec![None],
-        Strategy::Ground => Some(adf.grounded()),
+        Strategy::Ground => vec![Some(adf.grounded())],
-        // TODO: error handling if no such model exists!
+        Strategy::Complete => adf.complete().map(Some).collect(),
-        Strategy::FirstComplete => Some(adf.complete().next().unwrap()),
+        Strategy::Stable => adf.stable().map(Some).collect(),
-        // TODO: error handling if no such model exists!
+        // TODO: INPUT VALIDATION: only allow this for hybrid parsing
-        Strategy::FirstStable => Some(adf.stable().next().unwrap()),
+        Strategy::StableCountingA => adf.stable_count_optimisation_heu_a().map(Some).collect(),
-        // TODO: error handling if no such model exists!
+        // 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(
+        Strategy::StableNogood => adf
-            adf.stable_nogood(adf_bdd::adf::heuristics::Heuristic::default())
+            .stable_nogood(adf_bdd::adf::heuristics::Heuristic::default())
-                .next()
+            .map(Some)
-                .unwrap(),
+            .collect(),
-        ),
     };
 
-    let dto = adf.into_double_labeled_graph(ac.as_ref());
+    let dto: Vec<DoubleLabeledGraph> = acs
+        .iter()
+        .map(|ac| adf.into_double_labeled_graph(ac.as_ref()))
+        .collect();
 
     web::Json(dto)
 }