copilot-visualizer (empty) → 4.5
raw patch · 17 files changed
+1942/−0 lines, 17 filesdep +aesondep +basedep +copilotsetup-changed
Dependencies added: aeson, base, copilot, copilot-core, copilot-interpreter, copilot-language, copilot-visualizer, filepath, hint, ogma-extra, pretty, text, websockets
Files
- CHANGELOG +7/−0
- LICENSE +29/−0
- README.md +34/−0
- Setup.hs +2/−0
- copilot-visualizer.cabal +130/−0
- data/static_html/index.html +255/−0
- data/tikz/tikz.tex +37/−0
- examples/gui/Main.hs +20/−0
- examples/gui/copilot.css +50/−0
- examples/gui/copilot.js +489/−0
- examples/gui/main.html +67/−0
- examples/tikz/Heater.hs +37/−0
- src/Copilot/Visualize/Dynamic.hs +253/−0
- src/Copilot/Visualize/Live.hs +162/−0
- src/Copilot/Visualize/Static.hs +36/−0
- src/Copilot/Visualize/TypedTrace.hs +158/−0
- src/Copilot/Visualize/UntypedTrace.hs +176/−0
+ CHANGELOG view
@@ -0,0 +1,7 @@+2025-07-07+ * Version bump (4.5). (#642)+ * Include in mainline. (#624)++2025-06-26+ * Release 4.4. (copilot-visualizer#5)+ * Initial version. (copilot-visualizer#4)
+ LICENSE view
@@ -0,0 +1,29 @@+2024-2025 (c) NASA+BSD3 License terms++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++Redistributions of source code must retain the above copyright+notice, this list of conditions and the following disclaimer.++Redistributions in binary form must reproduce the above copyright+notice, this list of conditions and the following disclaimer in the+documentation and/or other materials provided with the distribution.++Neither the name of the developers nor the names of its contributors+may be used to endorse or promote products derived from this software+without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,34 @@+[](https://app.travis-ci.com/github/Copilot-Language/copilot)++# Copilot: a stream DSL++The visualizer, which draws Copilot specifications using different graphical+formats.++Copilot is a runtime verification framework written in Haskell. It allows the+user to write programs in a simple but powerful way using a stream-based+approach.++Programs can be interpreted for testing (with the library copilot-interpreter),+or translated C99 code to be incorporated in a project, or as a standalone+application. The C99 backend ensures us that the output is constant in memory+and time, making it suitable for systems with hard realtime requirements.++## Installation++Copilot-visualizer can be found on+[Hackage](https://hackage.haskell.org/package/copilot-interpreter). It is+typically only installed as part of the complete Copilot distribution. For+installation instructions, please refer to the [Copilot+website](https://copilot-language.github.io).++## Further information++For further information, install instructions and documentation, please visit+the Copilot website:+[https://copilot-language.github.io](https://copilot-language.github.io)++## License++Copilot is distributed under the BSD-3-Clause license, which can be found+[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-interpreter/LICENSE).
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot-visualizer.cabal view
@@ -0,0 +1,130 @@+cabal-version: >= 1.10+name: copilot-visualizer+version: 4.5+synopsis: Visualizer for Copilot.+description:+ Visualizer for Copilot.+ .+ Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in+ Haskell that compiles into embedded C. Copilot contains an interpreter,+ multiple back-end compilers, and other verification tools.+ .+ A tutorial, examples, and other information are available at+ <https://copilot-language.github.io>.++author: Ivan Perez, Frank Dedden, Ryan Scott, Kyle Beechly+license: BSD3+license-file: LICENSE+maintainer: Ivan Perez <ivan.perezdominguez@nasa.gov>+homepage: https://copilot-language.github.io+bug-reports: https://github.com/Copilot-Language/copilot/issues+stability: Experimental+category: Language, Embedded+build-type: Simple+extra-source-files: README.md+ CHANGELOG+ examples/gui/Main.hs+ examples/gui/main.html+ examples/gui/copilot.css+ examples/gui/copilot.js+ examples/tikz/Heater.hs++data-files: data/tikz/tikz.tex+ data/static_html/index.html++x-curation: uncurated++source-repository head+ type: git+ location: https://github.com/Copilot-Language/copilot.git+ subdir: copilot-visualizer++flag examples+ description: Enable examples+ default: False+ manual: True++library++ default-language:+ Haskell2010++ hs-source-dirs:+ src++ ghc-options:+ -Wall++ build-depends:+ base >= 4.9 && < 5,+ aeson >= 2.0.0.0 && < 2.3,+ filepath >= 1.4.2 && < 1.6,+ hint >= 0.9.0 && < 1.10,+ pretty >= 1.0 && < 1.2,+ ogma-extra >= 1.6.0 && < 1.7,+ text >= 1.2.3.1 && < 2.2,+ websockets >= 0.12.7 && < 0.14,++ copilot >= 4.5 && < 4.6,+ copilot-core >= 4.5 && < 4.6,+ copilot-interpreter >= 4.5 && < 4.6,+ copilot-language >= 4.5 && < 4.6++ exposed-modules:++ Copilot.Visualize.Live+ Copilot.Visualize.Static++ other-modules:++ Copilot.Visualize.Dynamic+ Copilot.Visualize.TypedTrace+ Copilot.Visualize.UntypedTrace+ Paths_copilot_visualizer++executable gui-example+ main-is:+ Main.hs++ default-language:+ Haskell2010++ hs-source-dirs:+ examples/gui++ ghc-options:+ -Wall++ build-depends:+ base >= 4.9 && < 5,++ copilot-visualizer++ if flag(examples)+ buildable: True+ else+ buildable: False++executable tikz-example+ main-is:+ Heater.hs++ default-language:+ Haskell2010++ hs-source-dirs:+ examples/tikz++ ghc-options:+ -Wall++ build-depends:+ base >= 4.9 && < 5,++ copilot >= 4.5 && < 4.6,+ copilot-visualizer++ if flag(examples)+ buildable: True+ else+ buildable: False
+ data/static_html/index.html view
@@ -0,0 +1,255 @@+<html>+ <head>+ <link rel="preconnect" href="https://fonts.gstatic.com/" crossorigin="" />+ <link+ rel="stylesheet"+ as="style"+ onload="this.rel='stylesheet'"+ href="https://fonts.googleapis.com/css2?display=swap&family=Noto+Sans%3Awght%40400%3B500%3B700%3B900&family=Space+Grotesk%3Awght%40400%3B500%3B700"+ />++ <title>Copilot Visualizer</title>++ <script src="https://cdn.tailwindcss.com?plugins=forms,container-queries" >+ </script>++ <script src="https://d3js.org/d3.v7.min.js">+ </script>+ <style>+ .axis path,+ .axis line {+ fill: none;+ stroke: #000;+ shape-rendering: crispEdges;+ }+ .label {+ font-size: 12px;+ }+ .bool-background {+ opacity: 0.3;+ }+ .hexagon {+ stroke: black;+ stroke-width: 1px;+ color: green;+ }+ .value-text {+ font-size: 10px;+ text-anchor: middle;+ dominant-baseline: middle;+ }+ .time-label {+ font-family: sans-serif;+ font-size: 12px;+ fill: black;+ }+ .grid-line {+ stroke: #ccc;+ stroke-width: 1;+ stroke-dasharray: 3,3;+ }+ </style>+ </head>+ <body>+ <div>+ <svg id="timeline"></svg>+ </div>++ <script>+ const margin = {top: 20, right: 20, bottom: 30, left: 100};+ const width = 960 - margin.left - margin.right;+ const height = 200 - margin.top - margin.bottom;+ const rowHeight = 40;+ num_rows = 0;+{{#adTraceElems}}+num_rows = num_rows + 1;+{{/adTraceElems}}+{{#adTraceElems}}+{{teName}}_ix = 0;+{{/adTraceElems}}++ // Sample data+ const data = {+{{#adTraceElems}}+{{teName}}: [+{{#teValues}}+{time: {{teName}}_ix++, value: {{#teIsBoolean}}{{tvValue}}{{/teIsBoolean}}{{#teIsFloat}}{{tvValue}}{{/teIsFloat}}{{^teIsBoolean}}{{^teIsFloat}}"{{tvValue}}"{{/teIsFloat}}{{/teIsBoolean}}, duration: 1},+{{/teValues}}+],+{{/adTraceElems}}+ };++ // Process numeric data to include duration and y-positions+ function processNumericData(data) {+ const maxValue = Math.max(...data.map(d => d.value));+ const minValue = Math.min(...data.map(d => d.value));+ const yScale = d3.scaleLinear()+ .domain([minValue, maxValue])+ .range([rowHeight * 0.8, rowHeight * 0.2]);++ return data.map((d, i) => ({+ ...d,+ duration: i < data.length - 1 ? data[i + 1].time - d.time : {{adLastSample}} + 1 - d.time,+ y: yScale(d.value)+ }));+ }++ // const processedNumericData = processNumericData(data.numericRow);++ // Create SVG+ const svg = d3.select("#timeline")+ .attr("width", width + margin.left + margin.right)+ .attr("height", (rowHeight * num_rows) + margin.top + margin.bottom)+ .append("g")+ .attr("transform", `translate(${margin.left},${margin.top})`);++ // Create scales+ const xScale = d3.scaleLinear()+ .domain([0, {{adLastSample}} + 1])+ .range([0, width]);++ // Create x-axis with ticks at integer positions+ const xAxis = d3.axisBottom(xScale)+ .tickValues(Array.from({length: 11}, (_, i) => i))+ .tickFormat('');++ // Add row labels+ const labels = [{{#adTraceElems}}"{{teName}}", {{/adTraceElems}} ];+ svg.selectAll(".label")+ .data(labels)+ .enter()+ .append("text")+ .attr("class", "label")+ .attr("x", -90)+ .attr("y", (d, i) => i * rowHeight + rowHeight/2)+ .text(d => d);++ // Function to create hexagon path+ function hexagonPath(width, height) {+ return `+ M ${width-10},0+ L ${width},${height/2}+ L ${width-10},${height}+ L ${10},${height}+ L ${0},${height/2}+ L ${10},0+ Z+ `;+ }++ // Draw boolean rows with colored backgrounds+ const drawBooleanRow = (data, rowIndex) => {+ const rowG = svg.append("g")+ .attr("transform", `translate(0,${rowIndex * rowHeight})`);++ // Draw colored backgrounds+ rowG.selectAll("rect")+ .data(data)+ .enter()+ .append("rect")+ .attr("class", "bool-background")+ .attr("x", d => xScale(d.time))+ .attr("y", 0)+ .attr("width", d => xScale(d.duration) - xScale(0))+ .attr("height", rowHeight)+ .attr("fill", d => d.value ? "#90EE90" : "#FFB6C1");+ };++ // Draw numeric row with stretched hexagons+ const drawNumericRow = (data, rowIndex) => {+ const rowG = svg.append("g")+ .attr("transform", `translate(0,${rowIndex * rowHeight})`);++ const hexHeight = rowHeight * 0.8;++ // Create hexagon groups+ const hexGroups = rowG.selectAll("g")+ .data(data)+ .enter()+ .append("g")+ .attr("transform", d => `translate(${xScale(d.time)},${rowHeight * 0.1})`);++ // Add hexagons+ hexGroups.append("path")+ .attr("class", "hexagon")+ .attr("d", d => hexagonPath(xScale(d.duration) - xScale(0), hexHeight))+ .attr("fill", "#f7fbff");++ // Add value text+ hexGroups.append("text")+ .attr("class", "value-text")+ .attr("x", d => (xScale(d.duration) - xScale(0)) / 2)+ .attr("y", hexHeight / 2)+ .text(d => d.value);+ };+++ // Draw all rows+ i = 0;+{{#adTraceElems}}+{{#teIsBoolean}}+drawBooleanRow(data.{{teName}}, i); i++;+{{/teIsBoolean}}+{{^teIsBoolean}}+drawNumericRow(processNumericData(data.{{teName}}), i); i++;+{{/teIsBoolean}}+{{/adTraceElems}}++ // Add the axis+ const axisGroup = svg.append("g")+ .attr("class", "axis")+ .attr("transform", `translate(0,${rowHeight * num_rows})`)+ .call(xAxis);++ // After creating the axis and labels, add vertical grid lines+ const gridLines = axisGroup.selectAll(".grid-line")+ .data(Array.from({length: 11}, (_, i) => i))+ .enter()+ .append("line")+ .attr("class", "grid-line")+ .attr("x1", d => xScale(d))+ .attr("x2", d => xScale(d))+ .attr("y1", -rowHeight * (num_rows + 1)) // Start from top (negative because we're going up from axis)+ .attr("y2", 0) // End at axis+ .style("stroke", "#ccc") // Light gray color+ .style("stroke-width", "1")+ .style("stroke-dasharray", "3,3"); // Creates dotted line++ // Add offset labels+ const timeLabels = axisGroup.selectAll(".time-label")+ .data(Array.from({length: num_rows + 1}, (_, i) => i))+ .enter()+ .append("text")+ .attr("class", "time-label")+ .attr("x", d => xScale(d + 0.5))+ .attr("y", 25)+ .attr("text-anchor", "middle")+ .text(d => d + "");++ // Detect clicks on timeline.+ svg.on("click", function(event) {+ const mouseX = d3.pointer(event)[0];+ const time = Math.floor(xScale.invert(mouseX).toFixed(2));+ const row = Math.floor((event.offsetY - margin.top) / rowHeight);+ const label = labels[row];++ console.log("Label:", label , "Time:", time);+ });++ // Detect mouse wheel on timeline.+ svg.on("wheel", function(event) {+ // Prevent default scroll behavior+ event.preventDefault();++ const mouseX = d3.pointer(event)[0];+ const time = Math.floor(xScale.invert(mouseX).toFixed(2));+ const row = Math.floor((event.offsetY - margin.top) / rowHeight);+ const label = labels[row];+ const dir = event.deltaY < 0 ? 'up' : 'down';++ console.log ( "Label:", label, "Time:", time, "Direction:", dir);+ });++ </script>+ </body>+</html>
+ data/tikz/tikz.tex view
@@ -0,0 +1,37 @@+{{=<% %>=}}+\documentclass{standalone}+\usepackage{tikz}+\usepackage{tikz-timing}+\usepackage{xcolor}+\definecolor{false}{HTML}{ECD9ED}+\definecolor{true}{HTML}{D9ECED}+\begin{document}+\newcommand{\true}{T}+\newcommand{\false}{F}+\tikzset{+every picture/.style={+ execute at end picture={+ \path (current bounding box.south west) +(-1,-1) (current bounding box.north east) +(1,1);+ }+}+}++\tikzset{+timing/.style={x=5ex,y=2ex},+timing/rowdist=4ex,+timing/dslope=0.1,+x=5ex,+timing/coldist=1ex,+timing/name/.style={font=\sffamily\scriptsize},+timing/d/text/.style={font=\sffamily\tiny},+}+\begin{tikztimingtable}+<%#adTraceElems%>+<%teName%> & g<%#teValues%><%#tvIsEmpty%>S<%/tvIsEmpty%><%^tvIsEmpty%><%#teIsBoolean%>[fill=<%tvValue%>]D{\<%tvValue%>}<%/teIsBoolean%><%^teIsBoolean%>D{<%tvValue%>}<%/teIsBoolean%><%/tvIsEmpty%><%/teValues%>\\+<%/adTraceElems%>+\extracode+\begin{background}[shift={(0.05,0)},help lines]+\vertlines[help lines,opacity=0.3]{-0.3ex,...,<%adLastSample%>}+\end{background}+\end{tikztimingtable}+\end{document}
+ examples/gui/Main.hs view
@@ -0,0 +1,20 @@+import Copilot.Visualize.Live++main = visualize spec++spec :: String+spec = unlines+ [ "let temperature :: Stream Word8"+ , " temperature = extern \"temperature\" (Just [0, 15, 20, 25, 30])"+ , ""+ , " ctemp :: Stream Float"+ , " ctemp = (unsafeCast temperature) * (150.0 / 255.0) - 50.0"+ , ""+ , " trueFalse :: Stream Bool"+ , " trueFalse = [True] ++ not trueFalse"+ , ""+ , "in do trigger \"heaton\" (temperature < 18) [arg ctemp, arg (constI16 1), arg trueFalse]"+ , " trigger \"heatoff\" (temperature > 21) [arg (constI16 1), arg ctemp]"+ , " observer \"temperature\" temperature"+ , " observer \"temperature2\" (temperature + 1)"+ ]
+ examples/gui/copilot.css view
@@ -0,0 +1,50 @@+/* Timeline */+/* Timeline decoration: Grid */+.axis path,+.axis line {+ fill: none;+ stroke: #000;+ shape-rendering: crispEdges;+}+.grid-line {+ stroke: #ccc;+ stroke-width: 1;+ stroke-dasharray: 3,3;+}++/* Timeline decoration: Labels */+.label {+ font-size: 12px;+}+.time-label {+ font-family: sans-serif;+ font-size: 12px;+ fill: black;+}+.value-text {+ font-size: 10px;+ text-anchor: middle;+ dominant-baseline: middle;+}++/* Timeline decoration: Values */+.hexagon {+ stroke: black;+ stroke-width: 1px;+ color: green;+}+.bool-background {+ opacity: 0.3;+}++/* Toolbar buttons */+button {+ width: 100px !important;+ height: 48px !important;+ border-radius: 24px !important;+ background-color: #f1316b !important;+ color: #fff !important;+ margin-top: 45px !important;+ border:none !important;+ font-size: 12px !important;+}
+ examples/gui/copilot.js view
@@ -0,0 +1,489 @@+/* Constants */++/* Timeline dimensions */+const margin = {top: 20, right: 20, bottom: 30, left: 90};+const width = 960 - margin.left - margin.right;+const height = 200 - margin.top - margin.bottom;+const rowHeight = 40;++/**+ * Position of the stream labels wrt. to the left side of the timeline.+ */+const labelPosX = -90;++/* Timeline colors */++/* Default colors for true and false (just dim green and red). */+const booleanColorDefaultTrue = "#90EE90";+const booleanColorDefaultFalse = "#FFB6C1";++/*+ * Alternative colors for true and false, making colored backgrounds more+ * easily distinguishable in conditions with reduced color. Specifically:+ *+ * - Increase blue content in the 'false' color to increase distinction from+ * the 'true' color in protanopic (no red) and deuteranopic (no green).+ *+ * - Decrease red content in the 'false' color to increase distinction from the+ * 'true' color in achromatopsic (no color) conditions.+ *+ * This does not meaningfully address visibility considerations in reduced+ * contrast or blurry conditions.+ */+const booleanColorHighContrastTrue = "#90EE90";+const booleanColorHighContrastFalse = "#E1B6ED";++/* Timeline state */+let svg;+let data = { adLastSample: 0, adTraceElems: [] };+let xScale;+let numRows = 0;+let numSteps = 2;+let booleanColorTrue = booleanColorDefaultTrue;+let booleanColorFalse = booleanColorDefaultFalse;++/**+ * Process numeric data, adding duration and y-positions to each trace element.+ */+function processNumericData(data)+{+ // Calculate bounds of stream.+ const maxValue = Math.max(...data.map(d => d.tvValue));+ const minValue = Math.min(...data.map(d => d.tvValue));++ // Vertical scale of the stream.+ const yScale = d3.scaleLinear()+ .domain([minValue, maxValue])+ .range([rowHeight * 0.8, rowHeight * 0.2]);++ // Return the data augmented with duration for each sample, and the vertical+ // scale.+ return data.map((d, i) => ({+ ...d,+ duration:+ i < data.length - 1 ? data[i + 1].time - d.time : numSteps + 1 - d.time,+ y: yScale(d.tvValue)+ }));+}++/**+ * Create timeline labels.+ */+function createLabels()+{+ document.querySelectorAll(".label").forEach(function(lst) {+ lst.remove();+ });++ // Add row labels.+ const labels = data.adTraceElems.map((x) => x.teName);+ svg.selectAll(".label")+ .data(labels)+ .enter()+ .append("text")+ .attr("class", "label")+ .attr("x", labelPosX)+ .attr("y", (d, i) => i * rowHeight + rowHeight/2)+ .text(d => d);+}++/**+ * Draw numeric row with stretched hexagons.+ */+function drawNumericRow(data, rowIndex)+{+ const rowG = svg.append("g")+ .attr("class", "value_list")+ .attr("transform", `translate(0,${rowIndex * rowHeight})`);++ const hexHeight = rowHeight * 0.8;++ time = 0;++ // Create hexagon groups.+ const hexGroups = rowG.selectAll("g")+ .data(data)+ .enter()+ .append("g")+ .attr("transform", d => `translate(${xScale(time++)},${rowHeight * 0.1})`);++ // Add hexagons.+ hexGroups.append("path")+ .attr("class", "hexagon")+ .attr("d", d => hexagonPath(xScale(1) - xScale(0), hexHeight))+ .attr("fill", "#f7fbff");++ // Add value text.+ hexGroups.append("text")+ .attr("class", "value-text")+ .attr("x", d => (xScale(1) - xScale(0)) / 2)+ .attr("y", hexHeight / 2)+ .text(d => d.tvValue);+}++/**+ * Draw boolean rows with colored backgrounds.+ */+function drawBooleanRow(data, rowIndex)+{+ const rowG = svg.append("g")+ .attr("class", "value_list")+ .attr("transform", `translate(0,${rowIndex * rowHeight})`);++ time = 0;++ // Draw colored backgrounds.+ rowG.selectAll("rect")+ .data(data)+ .enter()+ .append("rect")+ .attr("class", "bool-background")+ .attr("x", d => xScale(time++))+ .attr("y", 0)+ .attr("width", d => xScale(1) - xScale(0))+ .attr("height", rowHeight)+ .attr("fill", d => d.tvValue == "true" ? booleanColorTrue : booleanColorFalse);+}++/**+ * Re-draw complete timeline.+ */+function redraw()+{+ document.querySelectorAll(".value_list").forEach(function(lst) {+ lst.remove();+ });++ // Draw all rows.+ i = 0;+ data.adTraceElems.forEach(function(traceElem) {+ if (traceElem.teIsBoolean)+ {+ drawBooleanRow(traceElem.teValues, i);+ }+ else+ {+ drawNumericRow(processNumericData(traceElem.teValues), i);+ }+ i++;+ });+}++/**+ * Create SVG for the timeline.+ */+function createSVG()+{+ // Clear all existing elements.+ if (typeof svg !== 'undefined' ) { svg.selectAll("*").remove(); }++ // Calculate number of rows and columns (steps) from available data.+ numRows = data.adTraceElems.length;+ numSteps = data.adLastSample;++ // Create SVG.+ svg = d3.select("#timeline")+ .attr("width", width + margin.left + margin.right)+ .attr("height", (rowHeight * numRows) + margin.top + margin.bottom)+ .append("g")+ .attr("transform", `translate(${margin.left},${margin.top})`);++ // Create scales.+ xScale = d3.scaleLinear()+ .domain([0, numSteps + 1])+ .range([0, width]);++ // Create x-axis with ticks at integer positions.+ const xAxis = d3.axisBottom(xScale)+ .tickValues(Array.from({length: 11}, (_, i) => i))+ .tickFormat('');++ createLabels();+ redraw();++ // Add the axis.+ const axisGroup = svg.append("g")+ .attr("class", "axis")+ .attr("transform", `translate(0,${rowHeight * numRows})`)+ .call(xAxis);++ // After creating the axis and labels, add vertical grid lines.+ //+ // Use light gray as color, a dotted line, start from the top (negative+ // because we are going up from the axis), and end at the axis.+ const gridLines = axisGroup.selectAll(".grid-line")+ .data(Array.from({length: 11}, (_, i) => i))+ .enter()+ .append("line")+ .attr("class", "grid-line")+ .attr("x1", d => xScale(d))+ .attr("x2", d => xScale(d))+ .attr("y1", -rowHeight * (numRows + 1))+ .attr("y2", 0)+ .style("stroke", "#ccc")+ .style("stroke-width", "1")+ .style("stroke-dasharray", "3,3");++ // Add offset labels.+ const timeLabels = axisGroup.selectAll(".time-label")+ .data(Array.from({length: numRows + 1}, (_, i) => i))+ .enter()+ .append("text")+ .attr("class", "time-label")+ .attr("x", d => xScale(d + 0.5))+ .attr("y", 25)+ .attr("text-anchor", "middle")+ .text(d => d + "");++ // Detect clicks on timeline.+ svg.on("click", function(event) {+ const mouseX = d3.pointer(event)[0];+ const time = Math.floor(xScale.invert(mouseX).toFixed(2));+ const row = Math.floor((event.offsetY - margin.top) / rowHeight);+ const label = data.adTraceElems[row].teName;++ console.log("Label:", label , "Time:", time);+ ws.send('(Up ' + time + ', "' + label + '")');+ });++ // Detect mouse wheel on timeline.+ svg.on("wheel", function(event) {+ // Prevent default scroll behavior.+ event.preventDefault();++ const mouseX = d3.pointer(event)[0];+ const time = Math.floor(xScale.invert(mouseX).toFixed(2));+ const row = Math.floor((event.offsetY - margin.top) / rowHeight);+ const label = data.adTraceElems[row].teName;+ const dir = event.deltaY < 0 ? 'Up' : 'Down';++ ws.send('(' + dir + ' ' + time + ', "' + label + '")');++ console.log ( "Label:", label, "Time:", time, "Direction:", dir);+ });+}++/**+ * Add a step to the simulation.+ */+function stepUp()+{+ ws.send('(StepUp, "")');+}++/**+ * Reduce the number of steps of the simulation.+ */+function stepDown()+{+ ws.send('(StepDown, "")');+}++/**+ * Open a dialog requesting information to add a new stream to the simulation.+ */+function addStream()+{+ const popup = document.getElementById("popup");+ popup.classList.remove("hidden");+}++/**+ * Cancel dialog requesting information to add a new stream to the simulation.+ */+function closePopup()+{+ const popup = document.getElementById("popup");+ popup.classList.add("hidden");+}++/**+ * Add a new stream to the simulation. The definition provided must be correct+ * in the context of the current simulation, and the name given to the new+ * stream must be valid in Haskell, unique in the current context, and not+ * clash with any existing names.+ */+function addStreamSubmit()+{+ const popup = document.getElementById("popup");+ const inputName = document.getElementById("inputName").value;+ const inputExpr = document.getElementById("inputExpr").value;+ ws.send('(AddStream "' + inputName + '" "(' + inputExpr + ')", "")');+ popup.classList.add("hidden");+}++/**+ * Toggle the color scheme of the timeline.+ */+function toggleColors()+{+ const highContrastBtn = document.getElementById('high_contrast');+ if (highContrastBtn.checked) {+ booleanColorTrue = booleanColorHighContrastTrue;+ booleanColorFalse = booleanColorHighContrastFalse;+ } else {+ booleanColorTrue = booleanColorDefaultTrue;+ booleanColorFalse = booleanColorDefaultFalse;+ }++ createSVG();+}++/* Attach event handlers to UI elements */++// Somehow this does not work if we match the svg element directly, so we match+// the parent div.+document.getElementById("copyPNG").addEventListener("click", () => copyPNG("#timeline-parent"));++document.getElementById("copySVG").addEventListener("click", () => copySVG("#timeline"));++// Somehow this does not work if we match the svg element directly, so we match+// the parent div.+document.getElementById("downloadPNG").addEventListener("click", () => downloadPNG("#timeline-parent", "timeline"));++document.getElementById("downloadSVG").addEventListener("click", () => downloadSVG("#timeline", "timeline"));++document.getElementById("stepUp").addEventListener("click", stepUp);+document.getElementById("stepDown").addEventListener("click", stepDown);+document.getElementById("addStream").addEventListener("click", addStream);+document.getElementById("closePopup").addEventListener("click", closePopup);+document.getElementById("submitPopup").addEventListener("click", addStreamSubmit);++// Adjust colors using high-contrast when applicable.+document.getElementById('high_contrast').addEventListener('change', toggleColors);++createSVG();++// Communicate with the backend instance of Copilot via a websocket.+let ws = new WebSocket('ws://localhost:9160');++ws.onmessage = function(event) {+ data = JSON.parse(event.data);+ createSVG();+};++ws.onclose = function() {+ console.log('Disconnected from server');+};++ws.onerror = function(error) {+ console.log('Error: ' + error.message);+};++/* Auxiliary functions */++/**+ * Create an hexagon path (used for cells or samples).+ */+function hexagonPath(width, height)+{+ return `+ M ${width-10},0+ L ${width},${height/2}+ L ${width-10},${height}+ L ${10},${height}+ L ${0},${height/2}+ L ${10},0+ Z+ `;+}++/**+ * Download a file containing a given text.+ */+function download(filename, text)+{+ var element = document.createElement('a');+ element.setAttribute('href', 'data:text/plain;charset=utf-8,' + encodeURIComponent(text));+ element.setAttribute('download', filename);++ element.style.display = 'none';+ document.body.appendChild(element);++ element.click();++ document.body.removeChild(element);+}++/**+ * Copy element as SVG to clipboard as SVG.+ *+ * @param {svg} queryString - Query string referring to an SVG element in the+ * current document.+ */+function copySVG(queryString)+{+ const mySVG = document.querySelector(queryString);+ const data = new XMLSerializer().serializeToString(mySVG);++ navigator.clipboard.writeText(data).then(+ () => {+ console.log("SVG copied to clipboard");+ },+ (err) => {+ console.log("Failed to copy SVG to clipboard");+ }+ );+}++/**+ * Copy timeline to clipboard as PNG.+ *+ * @param {string} queryString - Query string referring to element in the+ * current document.+ */+function copyPNG(queryString)+{+ const elem = document.querySelector(queryString);+ html2canvas(elem).then(function(canvas) {+ canvas.toBlob(function(blob) {+ navigator.clipboard+ .write([+ new ClipboardItem(+ Object.defineProperty({}, blob.type, {+ value: blob,+ enumerable: true+ })+ )+ ]).then(function() {+ console.log("Copied to clipboard");+ });+ });+ });+}++/**+ * Download screenshot of an element as a PNG file.+ *+ * @param {string} queryString - Query string referring to element in the+ * current document.+ *+ * @param {string} defaultFilename - Default file name used in the save file+ * dialog.+ */+function downloadPNG(queryString, defaultFilename)+{+ const mySVG = document.querySelector(queryString);+ html2canvas(mySVG).then(function(canvas) {+ var a = document.createElement('a');+ a.href = canvas.toDataURL();+ a.download = defaultFilename + ".png";+ a.click();+ });+}++/**+ * Download screenshot of timeline as SVG file.+ *+ * @param {string} queryString - Query string referring to element in the+ * current document.+ *+ * @param {string} defaultFilename - Default file name used in the save file+ * dialog.+ */+function downloadSVG(queryString, defaultFilename)+{+ const mySVG = document.querySelector(queryString);+ const data = new XMLSerializer().serializeToString(mySVG);+ download(defaultFilename + ".svg", data);+}
+ examples/gui/main.html view
@@ -0,0 +1,67 @@+<html>+ <head>+ <title>Copilot Visualizer</title>++ <!-- Style sheets -->+ <link rel="preconnect" href="https://fonts.gstatic.com/" crossorigin="" />+ <link rel="stylesheet" as="style" onload="this.rel='stylesheet'" href="https://fonts.googleapis.com/css2?display=swap&family=Noto+Sans%3Awght%40400%3B500%3B700%3B900&family=Space+Grotesk%3Awght%40400%3B500%3B700" />+ <link rel="stylesheet" type="text/css" href="./copilot.css" />++ <!-- Scripts -->+ <!-- A copilot-specific script is loaded at the end of the body -->+ <script src="https://cdn.tailwindcss.com?plugins=forms,container-queries"></script>+ <script src="https://d3js.org/d3.v7.min.js"></script>+ <script src="https://cdnjs.cloudflare.com/ajax/libs/html2canvas/1.4.1/html2canvas.min.js"></script>+ </head>+ <body>+ <!-- Timeline -->+ <div id="timeline-parent" style="display: inline-block;" class="ml-4 mt-4" >+ <svg id="timeline"></svg>+ </div>++ <!-- Fixed button list under timeline -->+ <div class="ml-4">+ <button id="copyPNG">Copy as PNG</button>+ <button id="copySVG">Copy as SVG</button>+ <button id="downloadPNG">Save as PNG</button>+ <button id="downloadSVG">Save as SVG</button>+ <button id="stepUp">+1 step</button>+ <button id="stepDown">-1 step</button>+ <button id="addStream">Add Stream</button>+ </div>++ <!-- Toggle button for high-contrast mode -->+ <div class="ml-4 mt-4">+ <label class="flex items-center text">+ High-contrast mode+ <input type="checkbox" class="appearance-none sr-only peer" id="high_contrast" unchecked />+ <span class="w-12 h-7 flex items-center flex-shrink-0 ml-4 p-1 bg-gray-300 rounded-full duration-300 ease-in-out peer-checked:bg-green-400 after:w-5 after:h-5 after:bg-white after:rounded-full after:shadow-md after:duration-300 peer-checked:after:translate-x-5"></span>+ </label>+ </div>++ <!-- Pop up used to query new expressions to simulate -->+ <div id="popup" class="fixed inset-0 bg-black bg-opacity-50 flex items-center justify-center hidden">+ <div class="bg-white p-6 rounded-lg shadow-lg w-80 text-center">+ <!-- Label -->+ <h3 class="text-lg font-semibold mb-4">Enter new stream details</h3>++ <!-- Text boxes -->+ <input type="text" id="inputName" placeholder="Name" class="w-full p-2 border rounded-md mb-2">+ <input type="text" id="inputExpr" placeholder="Expression" class="w-full p-2 border rounded-md mb-4">++ <!-- Buttons -->+ <div class="flex justify-between">+ <button id="submitPopup" class="px-4 py-2 bg-green-500 text-white rounded-lg hover:bg-green-600">+ Add+ </button>+ <button id="closePopup" class="px-4 py-2 bg-red-500 text-white rounded-lg hover:bg-red-600">+ Cancel+ </button>+ </div>+ </div>+ </div>++ <!-- Copilot-specific routines -->+ <script src="./copilot.js"></script>+ </body>+</html>
+ examples/tikz/Heater.hs view
@@ -0,0 +1,37 @@+-- Copyright 2025 NASA+-- Copyright 2019 National Institute of Aerospace / Galois, Inc.++-- This is a simple example with basic usage. It implements a simple home+-- heating system: It heats when temp gets too low, and stops when it is high+-- enough. It read temperature as a byte (range -50C to 100C) and translates+-- this to Celsius.++module Main where++import Language.Copilot+import Copilot.Visualize.Static++import Prelude hiding ((>), (<))++-- External temperature as a byte, range of -50C to 100C+temp :: Stream Word8+temp = extern "temperature" (Just [ 10, 15, 18, 19, 25, 5, 45 ])++-- Calculate temperature in Celsius.+-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there+-- is no direct relation between Word8 and Float.+ctemp :: Stream Float+ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0++spec = do+ -- Triggers that fire when the ctemp is too low or too high,+ -- pass the current ctemp as an argument.+ trigger "heaton" (ctemp < 18.0) [arg ctemp]+ trigger "heatoff" (ctemp > 21.0) [arg ctemp]++-- Compile the spec and produce a LaTeX file in the current directory with a+-- Tikz drawing of the spec.+main :: IO ()+main = do+ spec' <- reify spec+ visualize 3 spec' "tikz" "."
+ src/Copilot/Visualize/Dynamic.hs view
@@ -0,0 +1,253 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- |+-- Copyright : (c) NASA, 2024-2025+-- License : BSD-style (see the LICENSE file in the distribution)+--+-- Allow loading Copilot specifications from strings and modifying them live.+--+-- An example of a spec that can be passed as argument to the live simulator+-- follows:+--+-- @+-- spec :: String+-- spec = unlines+-- [ "let temperature :: Stream Word8"+-- , " temperature = extern \"temperature\" (Just [0, 15, 20, 25, 30])"+-- , ""+-- , " ctemp :: Stream Float"+-- , " ctemp = (unsafeCast temperature) * (150.0 / 255.0) - 50.0"+-- , ""+-- , " trueFalse :: Stream Bool"+-- , " trueFalse = [True] ++ not trueFalse"+-- , ""+-- , "in do trigger \"heaton\" (temperature < 18) [arg ctemp, arg (constI16 1), arg trueFalse]"+-- , " trigger \"heatoff\" (temperature > 21) [arg (constI16 1), arg ctemp]"+-- , " observer \"temperature\" temperature"+-- , " observer \"temperature2\" (temperature + 1)"+-- ]+-- @+--+-- The imports are predefined.+module Copilot.Visualize.Dynamic+ ( simInit+ , simStep+ , SimulationSettings(..)+ , mkDefaultSimulationSettings+ , SimData(..)+ )+ where++-- External imports+import qualified Language.Haskell.Interpreter as HI+import Prelude hiding (div, not, (++), (<), (>))+import qualified Prelude++-- External imports: Copilot+import qualified Copilot.Core as Core+import Copilot.Language hiding (interpret, typeOf)+import Language.Copilot hiding (interpret, typeOf)++-- Internal imports+import Copilot.Visualize.TypedTrace++-- | Simulation data.+data SimData = SimData+ { simSteps :: Int -- ^ Number of steps to simulate.+ , simSpec :: Core.Spec -- ^ Copilot spec to simulate.+ , simString :: String -- ^ Textual representation of Copilot spec.+ }++-- | Initialize a simulation.+simInit :: SimulationSettings -> String -> IO SimData+simInit simulationSettings spec = do+ -- Load the spec, and save it so that it doesn't need to be reloaded if it+ -- doesn't change.+ let numSteps = simulationSettingsInitialSteps simulationSettings+ spec' <- readSpec simulationSettings spec+ let simData = SimData numSteps spec' spec+ return simData++-- | Update the spec based on the input command received.+simStep :: SimulationSettings+ -> SimData+ -> (Command, String)+ -> IO SimData+simStep _ simData (StepUp, _) =+ pure simData { simSteps = simSteps simData + 1 }++simStep _ simData (StepDown, _) =+ pure simData { simSteps = simSteps simData + 1 }++simStep simulationSettings simData (AddStream name expr, _) = do+ let specN = concat [ simString simData, "\n", " ", completeExpr]++ completeExpr = concat [ "observer ", show name, " (", expr, ")" ]++ let trace = extractTrace $ simSpec simData+ spec2 <- readSpec simulationSettings specN+ let spec3 = updateWithTrace trace spec2++ pure simData { simSpec = spec3, simString = specN }++simStep simulationSettings simData (command, name) = do+ spec' <- apply simulationSettings (simSpec simData) name command+ pure simData { simSpec = spec' }++-- | Settings used for a simulation.+data SimulationSettings = SimulationSettings+ { simulationSettingsInitialSteps :: Int+ , simulationSettingsImports :: [(String, Maybe String)]+ }++-- | Default settings that simulates 3 steps and provides default imports of+-- the main Copilot modules.+mkDefaultSimulationSettings :: SimulationSettings+mkDefaultSimulationSettings =+ SimulationSettings+ 3+ [ ("Control.Monad.Writer", Nothing)+ , ("Copilot.Language", Nothing)+ , ("Copilot.Language.Spec", Nothing)+ , ("Data.Functor.Identity", Nothing)+ , ("Language.Copilot", Nothing)+ , ("Prelude", Just "P")+ ]++-- * Commands++-- * Load specs from strings++-- | Read a specification from a string and reify it.+readSpec :: SimulationSettings -> String -> IO Core.Spec+readSpec settings spec = do+ r <- HI.runInterpreter (loadSpec settings spec)+ case r of+ Left err -> do putStrLn $ "Error: " Prelude.++ show err+ error $ show err+ Right s -> return s++-- | Load a spec from a string, adding standard imports.+loadSpec :: SimulationSettings -> String -> HI.Interpreter Core.Spec+loadSpec settings spec = do+ HI.setImportsQ (simulationSettingsImports settings)+ spec' <- HI.interpret spec (HI.as :: Spec)+ HI.liftIO $ reify spec'++-- | Commands to apply to a running simulation.+data Command = StepUp+ | StepDown+ | Up Int+ | Down Int+ | AddStream String String+ | Noop+ deriving (Eq, Read, Show)++-- | Apply a command to a simulation.+apply :: SimulationSettings -> Core.Spec -> String -> Command -> IO Core.Spec+apply settings spec _name (AddStream sName sExpr) = do+ spec' <- addStream settings sName sExpr+ -- TODO: I need to bring the streams from the other spec too, otherwise the+ -- streams to include may refer to streams by ID that are in a different+ -- scope.+ let observers' = Core.specObservers spec'+ observers = Core.specObservers spec+ return $ spec { Core.specObservers = observers Prelude.++ observers' }++apply _settings spec name command = pure $ spec+ { Core.specStreams =+ map (updateStream name command) (Core.specStreams spec)+ , Core.specObservers =+ map (updateObserver name command) (Core.specObservers spec)+ , Core.specTriggers =+ map (updateTrigger name command) (Core.specTriggers spec)+ }++-- | Apply a command to an observer.+updateObserver :: String -> Command -> Core.Observer -> Core.Observer+updateObserver name command (Core.Observer i e ty) =+ Core.Observer i (updateExpr name command e) ty++-- | Apply a command to a trigger.+updateTrigger :: String -> Command -> Core.Trigger -> Core.Trigger+updateTrigger name command (Core.Trigger i e es) = Core.Trigger i e' es'+ where+ e' = updateExpr name command e+ es' = map (updateUExpr name command) es++-- | Apply a command to a core expression.+updateExpr :: String -> Command -> Core.Expr a -> Core.Expr a+updateExpr name command expr = case expr of+ Core.ExternVar ty nameE vs+ | nameE Prelude.== name+ -> Core.ExternVar ty nameE (updateValues vs ty command)++ | otherwise+ -> expr++ Core.Op1 op expr1 ->+ Core.Op1 op (updateExpr name command expr1)++ Core.Op2 op expr1 expr2 ->+ Core.Op2 op (updateExpr name command expr1) (updateExpr name command expr2)++ Core.Op3 op expr1 expr2 expr3 ->+ Core.Op3+ op+ (updateExpr name command expr1)+ (updateExpr name command expr2)+ (updateExpr name command expr3)++ _ -> expr++-- | Apply a command to an untyped expression that carries the information+-- about the type of the expression as a value (existential).+updateUExpr :: String -> Command -> Core.UExpr -> Core.UExpr+updateUExpr name cmd (Core.UExpr ty expr) =+ Core.UExpr ty (updateExpr name cmd expr)++-- | Apply a command to a stream.+updateStream :: String -> Command -> Core.Stream -> Core.Stream+updateStream name command (Core.Stream i buf expr ty) =+ Core.Stream i buf (updateExpr name command expr) ty++-- | Apply a command to a series of typed values, if any.+updateValues :: Maybe [a] -> Type a -> Command -> Maybe [a]+updateValues vsM ty command =+ fmap (fmap (updateValue command ty) . zip [0..]) vsM++-- | Apply a command to a typed value.+updateValue :: Command -> Type a -> (Int, a) -> a+updateValue (Up n) Core.Bool (ix, a) =+ if n Prelude.== ix then Prelude.not a else a+updateValue (Down n) Core.Bool (ix, a) =+ if n Prelude.== ix then Prelude.not a else a+updateValue (Up n) Core.Word8 (ix, a) =+ if n Prelude.== ix then a + 1 else a+updateValue (Down n) Core.Word8 (ix, a) =+ if n Prelude.== ix then a - 1 else a+updateValue _ _ (_, a) = a++-- * Sample spec++-- | Produce a specification from the expression for a stream.+addStream :: SimulationSettings -> String -> String -> IO Core.Spec+addStream settings name expr = do+ r <- HI.runInterpreter (addStream' settings name expr)+ case r of+ Left err -> do putStrLn $ "Error: " Prelude.++ show err+ error $ show err+ Right spec -> return spec++-- | Produce a specification from the expression for a stream, in an+-- interpreter context.+--+-- Observe that Interpreter () is an alias for InterpreterT IO ()+addStream' :: SimulationSettings -> String -> String -> HI.Interpreter Core.Spec+addStream' settings name expr = do+ HI.setImportsQ (simulationSettingsImports settings)+ let completeExpr = concat [ "observer ", show name, " (", expr, ")" ]++ spec <- HI.interpret completeExpr (HI.as :: Spec)+ HI.liftIO $ reify spec
+ src/Copilot/Visualize/Live.hs view
@@ -0,0 +1,162 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}+-- |+-- Copyright : (c) NASA, 2024-2025+-- License : BSD-style (see the LICENSE file in the distribution)+--+-- Run a Copilot simulation live and allow interacting with it using a+-- websocket.+--+-- This visualizer enables adding new streams to a visualization. To do so, the+-- visualizer needs access to the original spec, and needs to be able to+-- interpret new expressions in the same context as the prior expressions.+--+-- An example of a spec that can be passed as argument to the visualizer+-- follows:+--+-- @+-- spec :: String+-- spec = unlines+-- [ "let temperature :: Stream Word8"+-- , " temperature = extern \"temperature\" (Just [0, 15, 20, 25, 30])"+-- , ""+-- , " ctemp :: Stream Float"+-- , " ctemp = (unsafeCast temperature) * (150.0 / 255.0) - 50.0"+-- , ""+-- , " trueFalse :: Stream Bool"+-- , " trueFalse = [True] ++ not trueFalse"+-- , ""+-- , "in do trigger \"heaton\" (temperature < 18) [arg ctemp, arg (constI16 1), arg trueFalse]"+-- , " trigger \"heatoff\" (temperature > 21) [arg (constI16 1), arg ctemp]"+-- , " observer \"temperature\" temperature"+-- , " observer \"temperature2\" (temperature + 1)"+-- ]+-- @+--+-- The imports are predefined.+module Copilot.Visualize.Live+ ( visualize+ , visualizeWith+ , VisualSettings(..)+ , mkDefaultVisualSettings+ , SimulationSettings(..)+ , mkDefaultSimulationSettings+ )+ where++-- External imports+import Control.Exception (SomeException (..), handle)+import Data.Aeson (ToJSON (..), encode)+import qualified Data.Text as T+import qualified Network.WebSockets as WS+import Prelude hiding (div, not, (++), (<), (>))+import qualified Prelude+import Text.Read (readMaybe)++-- External imports: Copilot+import qualified Copilot.Core as Core+import Copilot.Interpret.Eval (ShowType (Haskell), eval)+import Copilot.Language hiding (interpret, typeOf)+import Copilot.Visualize.UntypedTrace (AppData, makeTraceEval)++-- Internal imports+import Copilot.Visualize.Dynamic++-- | Start a simulation for an input spec, listening for commands and+-- communicating the status via a websocket.+visualize :: String -> IO ()+visualize = visualizeWith mkDefaultVisualSettings++-- | Start a simulation for an input spec, listening for commands and+-- communicating the status via a websocket.+visualizeWith :: VisualSettings -> String -> IO ()+visualizeWith settings spec = do+ putStrLn $ concat+ [ "WebSocket server starting on port "+ , show (visualSettingsPort settings)+ , "..."+ ]+ WS.runServer+ (visualSettingsHost settings)+ (visualSettingsPort settings)+ (app settings spec)++-- | Settings used to customize the simulation and interaction.+data VisualSettings = VisualSettings+ { visualSettingsHost :: String+ -- ^ Host interface to listen to. Use+ -- "127.0.0.1" to listen at localhost.++ , visualSettingsPort :: Int+ -- ^ Port to listen to.++ , visualSettingsSimulation :: SimulationSettings+ -- ^ Settings for the simulation.+ }++-- | Default settings that simulates 3 steps and listens on localhost at port+-- 9160.+mkDefaultVisualSettings :: VisualSettings+mkDefaultVisualSettings = VisualSettings+ { visualSettingsHost = "127.0.0.1"+ , visualSettingsPort = 9160+ , visualSettingsSimulation = mkDefaultSimulationSettings+ }++-- * Server++-- | Server application using web sockets.+app :: VisualSettings -> String -> WS.ServerApp+app settings spec pending = do+ conn <- WS.acceptRequest pending+ WS.withPingThread conn 30 (return ()) $ appInit settings spec conn++-- | Initialize the backend.+appInit :: VisualSettings -> String -> WS.Connection -> IO ()+appInit settings spec conn = handle appException $ do+ -- Initialize the simulation.+ simData <- simInit (visualSettingsSimulation settings) spec++ -- Communicate the current values of the trace, in JSON, via the web+ -- socket.+ let appData = mkAppData (simSteps simData) (simSpec simData)+ let samples = encode $ toJSON appData+ WS.sendTextData conn samples++ -- Start the application loop.+ appMainLoop settings conn simData++ where++ appException :: SomeException -> IO ()+ appException e = do+ putStrLn $ "Error:" Prelude.++ show e+ error $ show e++-- | Run the main application, repeatedly reading commands from a web socket+-- and returning results via the same web socket.+appMainLoop :: VisualSettings+ -> WS.Connection+ -> SimData+ -> IO ()+appMainLoop settings conn simData = do+ -- Read a command from the web socket.+ cmdM <- readMaybe . T.unpack <$> WS.receiveData conn++ -- Run a simulation step, if a command has been received.+ let simulationSettings = visualSettingsSimulation settings+ simData' <- maybe (pure simData) (simStep simulationSettings simData) cmdM++ -- Communicate the current values of the trace, in JSON, via the web socket.+ let appData = mkAppData (simSteps simData') (simSpec simData')+ samples = encode $ toJSON appData+ WS.sendTextData conn samples++ appMainLoop settings conn simData'++-- * Auxiliary functions++-- | Obtain the trace data from a Copilot spec for a number of steps.+mkAppData :: Int -> Core.Spec -> AppData+mkAppData numSteps spec' =+ makeTraceEval numSteps spec' (eval Haskell numSteps spec')
+ src/Copilot/Visualize/Static.hs view
@@ -0,0 +1,36 @@+-- |+-- Copyright : (c) NASA, 2024-2025+-- License : BSD-style (see the LICENSE file in the distribution)+--+-- Produce a visual representation of a Copilot specification.+module Copilot.Visualize.Static+ ( visualize+ )+ where++-- External imports+import Data.Aeson (ToJSON (..))+import System.Directory.Extra (copyTemplate)+import System.FilePath ((</>))++-- External imports: Copilot+import Copilot.Core (Spec (..))+import Copilot.Interpret.Eval (ShowType (Haskell), eval)++-- Internal imports+import Copilot.Visualize.UntypedTrace (makeTraceEval)+import Paths_copilot_visualizer (getDataDir)++-- | Produce a visual representation of a Copilot specification, for a given+-- number of steps, using a template.+visualize :: Int -- ^ Number of steps to interpret.+ -> Spec -- ^ Specification to interpret.+ -> String -- ^ Base used to expand the static file (i.e., @"tikz"@,+ -- @"static_html"@).+ -> FilePath+ -> IO ()+visualize k spec base target = do+ dir <- getDataDir+ let f = dir </> "data" </> base+ let subs = toJSON $ makeTraceEval k spec $ eval Haskell k spec+ copyTemplate f subs target
+ src/Copilot/Visualize/TypedTrace.hs view
@@ -0,0 +1,158 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- |+-- Copyright : (c) NASA, 2024-2025+-- License : BSD-style (see the LICENSE file in the distribution)+--+-- Read and modify traces of specifications.+--+-- In the context of this module, a trace refers only to the values of+-- externs, since the state of a spec can be reproduced if the values of+-- externs are known.+module Copilot.Visualize.TypedTrace+ ( extractTrace+ , updateWithTrace+ , Trace(..)+ , UValues(..)+ )+ where++-- External imports+import Data.List hiding ((++))+import Data.Maybe (fromMaybe)+import qualified Data.Type.Equality as DE+import Data.Typeable (Typeable)+import Prelude hiding (div, not, (++), (<), (>))++-- External imports: Copilot+import qualified Copilot.Core as Core+import Language.Copilot hiding (interpret, typeOf)++-- | Map stream names to their values.+newtype Trace = Trace+ { traceMap :: [ (String, UValues) ]+ }++-- | Existentially typed list of values of a stream.+data UValues = forall a . Typeable a => UValues+ { uvType :: Core.Type a+ , uvValues :: [ a ]+ }++-- | Extract a trace from a core specification.+extractTrace :: Core.Spec -> Trace+extractTrace spec = Trace $ concat $ concat+ [ fmap extractTraceStream (Core.specStreams spec)+ , fmap extractTraceObserver (Core.specObservers spec)+ , fmap extractTraceTrigger (Core.specTriggers spec)+ ]++-- | Extract the values of a core 'Stream'.+extractTraceStream :: Core.Stream -> [ (String, UValues) ]+extractTraceStream (Core.Stream _id _buf expr _ty) =+ extractTraceExpr expr++-- | Extract the values of a core 'Observer'.+extractTraceObserver :: Core.Observer -> [ (String, UValues) ]+extractTraceObserver (Core.Observer _name expr _ty) =+ extractTraceExpr expr++-- | Extract the values of a core 'Trigger'.+extractTraceTrigger :: Core.Trigger -> [ (String, UValues) ]+extractTraceTrigger (Core.Trigger _name expr args) = concat $+ extractTraceExpr expr+ : fmap extractTraceUExpr args++-- | Extract the values of a core 'Expr'.+extractTraceExpr :: Core.Expr a -> [ (String, UValues) ]+extractTraceExpr (Core.Local _ _ _ expr1 expr2) = concat+ [ extractTraceExpr expr1+ , extractTraceExpr expr2+ ]+extractTraceExpr (Core.ExternVar ty name values) =+ [ (name, UValues ty (fromMaybe [] values)) ]+extractTraceExpr (Core.Op1 _op expr) =+ extractTraceExpr expr+extractTraceExpr (Core.Op2 _op expr1 expr2) = concat+ [ extractTraceExpr expr1+ , extractTraceExpr expr2+ ]+extractTraceExpr (Core.Op3 _op expr1 expr2 expr3) = concat+ [ extractTraceExpr expr1+ , extractTraceExpr expr2+ , extractTraceExpr expr3+ ]+extractTraceExpr (Core.Label _ty _lbl expr) =+ extractTraceExpr expr+extractTraceExpr _ = []++-- | Extract the values of a core 'UExpr'.+extractTraceUExpr :: Core.UExpr -> [ (String, UValues) ]+extractTraceUExpr (Core.UExpr ty expr) = extractTraceExpr expr++-- | Update externs in a spec.+updateWithTrace :: Trace -> Core.Spec -> Core.Spec+updateWithTrace trace spec = spec+ { Core.specStreams =+ fmap (updateWithTraceStream trace) (Core.specStreams spec)+ , Core.specObservers =+ fmap (updateWithTraceObserver trace) (Core.specObservers spec)+ , Core.specTriggers =+ fmap (updateWithTraceTrigger trace) (Core.specTriggers spec)+ }++-- | Update the values of a 'Stream' based on an input trace.+updateWithTraceStream :: Trace -> Core.Stream -> Core.Stream+updateWithTraceStream trace (Core.Stream ident buf expr ty) =+ Core.Stream ident buf (updateWithTraceExpr trace expr) ty++-- | Update the values of an 'Observer' based on an input trace.+updateWithTraceObserver :: Trace -> Core.Observer -> Core.Observer+updateWithTraceObserver trace (Core.Observer name expr ty) =+ Core.Observer name (updateWithTraceExpr trace expr) ty++-- | Update the values of a 'Trigger' based on an input trace.+updateWithTraceTrigger :: Trace -> Core.Trigger -> Core.Trigger+updateWithTraceTrigger trace (Core.Trigger name expr args) =+ Core.Trigger+ name+ (updateWithTraceExpr trace expr)+ (fmap (updateWithTraceUExpr trace) args)++-- | Update the values of an 'Expr' based on an input trace.+updateWithTraceExpr :: Trace -> Core.Expr a -> Core.Expr a+updateWithTraceExpr trace (Core.Local ty1 ty2 name expr1 expr2) =+ Core.Local+ ty1+ ty2+ name+ (updateWithTraceExpr trace expr1)+ (updateWithTraceExpr trace expr2)+updateWithTraceExpr trace (Core.ExternVar ty name values) =+ Core.ExternVar ty name values'+ where+ values' | Just (UValues ty2 vals) <- lookup name (traceMap trace)+ , Just DE.Refl <- DE.testEquality ty ty2+ = Just vals+ | otherwise+ = values+updateWithTraceExpr trace (Core.Op1 op expr) =+ Core.Op1 op (updateWithTraceExpr trace expr)+updateWithTraceExpr trace (Core.Op2 op expr1 expr2) =+ Core.Op2 op+ (updateWithTraceExpr trace expr1)+ (updateWithTraceExpr trace expr2)+updateWithTraceExpr trace (Core.Op3 op expr1 expr2 expr3) =+ Core.Op3 op+ (updateWithTraceExpr trace expr1)+ (updateWithTraceExpr trace expr2)+ (updateWithTraceExpr trace expr3)+updateWithTraceExpr trace (Core.Label ty lbl expr) =+ Core.Label ty lbl (updateWithTraceExpr trace expr)+updateWithTraceExpr trace x = x++-- | Update the values of a 'UExpr' based on an input trace.+updateWithTraceUExpr :: Trace -> Core.UExpr -> Core.UExpr+updateWithTraceUExpr trace (Core.UExpr ty expr) =+ Core.UExpr ty (updateWithTraceExpr trace expr)
+ src/Copilot/Visualize/UntypedTrace.hs view
@@ -0,0 +1,176 @@+{-# LANGUAGE DeriveGeneric #-}+-- |+-- Copyright : (c) NASA, 2024-2025+-- License : BSD-style (see the LICENSE file in the distribution)+--+-- Abstract representation of a trace as a series named streams with their+-- values, together with functions needed to convert a 'Spec' into a trace.+--+-- This trace is flat (untyped). Information about the types is captured+-- using boolean flags. This kind of trace is most useful to render values+-- on in logicless templates, since they don't have the capability to examine+-- the Haskell types.+module Copilot.Visualize.UntypedTrace+ ( AppData(..)+ , Trace+ , TraceElem(..)+ , TraceValue(..)+ , makeTraceEval+ )+ where++-- External imports+import Data.Aeson (ToJSON (..))+import Data.Bifunctor (second)+import Data.List (find, transpose)+import Data.Maybe (isJust, isNothing)+import GHC.Generics (Generic)+import Text.Printf (printf)+import Text.Read (readMaybe)++-- External imports: Copilot+import Copilot.Core (Spec (..), triggerArgs, triggerName)+import Copilot.Interpret.Eval (ExecTrace, Output, interpObservers,+ interpTriggers)++-- * Abstract representation of a trace++-- | Data related to a specification.+data AppData = AppData+ { adTraceElems :: Trace+ , adLastSample :: Int+ }+ deriving (Generic, Show)++instance ToJSON AppData++-- | A trace, defined by a list of trace elements, each defining a stream (in+-- an abstract sense).+type Trace = [ TraceElem ]++-- | An element of a trace, or stream, with a name, its values, and information+-- about its type, needed to render it correctly.+data TraceElem = TraceElem+ { teName :: String+ , teIsBoolean :: Bool+ , teIsFloat :: Bool+ , teValues :: [ TraceValue ]+ }+ deriving (Generic, Show)++instance ToJSON TraceElem++-- | An individual sample, with a value and an indication of whether the sample+-- exists.+data TraceValue = TraceValue+ { tvValue :: String+ , tvIsEmpty :: Bool+ }+ deriving (Generic, Show)++instance ToJSON TraceValue++-- | Generate an abstract representation of a trace of a specification+-- interpreted for a given number of steps.+makeTraceEval :: Int+ -> Spec+ -> ExecTrace+ -> AppData+makeTraceEval k spec e =+ AppData (observerTEs ++ triggerTEs) (k - 1)+ where+ observerTEs = map mkTraceElem (interpObserversOpt spec e)+ triggerTEs = map mkTraceElem (interpTriggersWithArgs spec e)++-- | Generate an element of a trace from a stream name and its values over+-- time.+mkTraceElem :: (String, [Maybe Output]) -> TraceElem+mkTraceElem (name, outputs) = TraceElem+ { teName = name+ , teValues = values+ , teIsBoolean = any (isBoolean . tvValue) values+ , teIsFloat = any (isFloat . tvValue) values+ }+ where+ values = map mkTraceValue outputs++-- | Generate an individual value (sample) of a trace.+mkTraceValue :: Maybe Output -> TraceValue+mkTraceValue x = TraceValue (showValue x) (isNothing x)++-- * Auxiliary functions++-- | Compute the list of values associated to observers.+interpObserversOpt :: Spec -> ExecTrace -> [(String, [Maybe Output])]+interpObserversOpt _spec = map (second (map Just)) . interpObservers++-- | Compute the list of values associated to triggers and their arguments.+--+-- For each trigger, we first include the values of the trigger itself, and+-- then the values of the arguments to the trigger.+interpTriggersWithArgs :: Spec -> ExecTrace -> [(String, [Maybe Output])]+interpTriggersWithArgs spec = concatMap triggerOutputs . interpTriggers+ where+ -- This function adds one more output for the trigger itself.+ triggerOutputs :: (String, [Maybe [Output]]) -> [(String, [Maybe Output])]+ triggerOutputs (triggerName, triggerArgs) =+ (triggerName, triggerValues) : zip argNames argValues+ where+ triggerValues = map triggerValue triggerArgs++ -- Value for the trigger at a given time, based on the values of its+ -- arguments.+ triggerValue :: Maybe [Output] -> Maybe Output+ triggerValue Nothing = Just "false"+ triggerValue (Just _) = Just "true"++ -- Names and values for the arguments.+ argNames = map (\ix -> triggerName ++ "Arg" ++ show ix) [0..]+ argValues = transpose (transMaybes numArgs triggerArgs)+ numArgs = triggerNumArgs spec triggerName++-- Number of arguments to a trigger in a spec.+--+-- PRE: name exists as a trigger in spec.+triggerNumArgs :: Spec -> String -> Int+triggerNumArgs spec name =+ case find (\t -> triggerName t == name) (specTriggers spec) of+ Nothing -> error "Couldn't find given trigger in spec, should never occur!"+ Just t -> length $ triggerArgs t++-- | True if the input value denotes a boolean value.+isBoolean :: String -> Bool+isBoolean "true" = True+isBoolean "false" = True+isBoolean _ = False++-- | True if the input value denotes a floating point value.+isFloat :: String -> Bool+isFloat s = isJust asInt || isJust asFloat+ where+ asInt :: Maybe Int+ asInt = readMaybe s++ asFloat :: Maybe Float+ asFloat = readMaybe s++-- | Show a value.+showValue :: Maybe Output -> String+showValue Nothing = "--"+showValue (Just s) | isFloat s = showValueFloat s+ | otherwise = s++-- | Show a floating point value.+showValueFloat :: Output -> String+showValueFloat = formatFloat . read+ where+ formatFloat :: Double -> String+ formatFloat = printf "%.2g"++-- | Given a list of maybe lists of known length, this function creates a list+-- of lists, pushing the Maybe's inside.+transMaybes :: Int -> [Maybe [a]] -> [[Maybe a]]+transMaybes = map . transMaybes'+ where+ transMaybes' argsLength (Just xs) = map Just xs+ transMaybes' argsLength Nothing = replicate argsLength Nothing