You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Thank you for your reply. For an example, consider an air-lock on a spacecraft, two doors and an intermediate chamber. How does Copilot remember if the chamber is pressurizing or depressurizing?
You could have the trigger functions modify a state global variable. I was wondering if there was a better approach, say with Temporal Logic?
Edit: the use case is a charging protocol on an electric vehicle (i.e. voltage instead of pressure).
I was hoping to have more time to clean this and improve it, but you've been patiently waiting for over 2 months now, so I'd rather keep things moving than stall this forever. Perfect is the enemy of good!
You can write state machines manually as follows. Let's imagine that you have an incoming stream of inputs with possible values 1, 2 and 3 ONLY:
More generally, here are three possible ways of implementing state machines, depending on whether you consider the existence of a state denoting an error or not, and whether you want all inputs to produce a transition or not.
Before immediately including this, perhaps it would pay off to 1) pick a representation that allows us to analyze the state machine first and ensure it's defined correctly, and 2) pick a Copilot implementation that generates more optimal code.
I was very glad to see your reply. Thank you very much for these examples, they're gold to someone just starting out with haskell.
In my use case, it turns out the FSM is managed by another controller and we just need to track its state and do stuff when some transitions occur. So the Copilot code turned out to be very simple; mostly externs and boolean operations.
Are there any downsides to tracking the state within Copilot, as opposed to updating a byte in the trigger functions? What if we want to resume the FSM from flash memory? Is the step() function normally stateless? My guess at the upside is the FSM operation can be proven easier?
So the Copilot code turned out to be very simple; mostly externs and boolean operations.
Great!
Are there any downsides to tracking the state within Copilot, as opposed to updating a byte in the trigger functions?
What do you mean by "Updating a byte in the trigger function"?
What if we want to resume the FSM from flash memory?
This presents an interesting use case that, to the best of my knowledge, has never been studied within Copilot. My first thought is that it may be possible by enclosing any stateful streams in an ifThenElse as follows:
The idea being that, when you want to resume from Flash memory, you just need to set the saved state in a global saved_state, set reset to true, and then call step().
Is the step() function normally stateless?
In general, you cannot assume that successive calls to step() are stateless. Each call advances streams one step, and they can refer to past values, so they can be stateful. This is a property of all stream-based or reactive languages (e.g., FRP).
My guess at the upside is the FSM operation can be proven easier?
You'd have a guarantee that the code generated is hard realtime.
You might also be able to prove certain properties of your FSM if you write it in Copilot, by leveraging the facilities of copilot-theorem, but I haven't done it. I'd be interested to see which properties you might want to prove.
You could of course define FSMs in Haskell using an existing library or custom representation, prove whatever you want statically, and then synthesize a Copilot FSM.
If you are operating in a safety-critical environment, then I'd suggest going down the route of trying to prove your FSM correct.
Thank you for your answers. Understanding Copilot as a FRP is really cool and it makes a lot more sense for implementing FSMs than what I led myself to believe. I'm looking forward to using and further understanding these FSM APIs you've shared here.
This question might on a bit of a tangent: is it possible/advisable to map Stream Word8 to Haskell's data types? (e.g. encode a state with Idle instead of 1)?
We've historically used integers and constants instead of enums. You can already use them to some extent, so long as you reduce the final result to word/ints using fromEnum and toEnum.
I suspect extending Copilot to support any Enums would be simple; you'd mainly need to know what underlying type can be used to represent the enum based on its size. I'd have to look into it in more detail. Related to #36, #58.
It pains me to say this, but I haven't made any progress because the client has settled with IQANdesign for now. I haven't been able to convince them of the importance of verified, portable code.
I am considering using Copilot for my next project to interpret user-customizable control-flow models. However, my focus has been on the lower levels so far.
I've just looked back over your FSM API proposal and your post made a lot more sense to me this time. I can't think of anything else it could need. Does it handle nesting? Clock delays? Preemptive interruption? Is it an RTOS? 🦋
It pains me to say this, but I haven't made any progress because the client has settled with IQANdesign for now. I haven't been able to convince them of the importance of verified, portable code.
That's absolutely ok. On the one hand, it may just be a better fit for their use case, and that's understandable. On the other, knowing more about this could help us improve in the future.
Has the reasoning behind this been one of user experience? Documentation? Anything else?
For what is worth, I've worked on automatically transforming SysML diagrams to Haskell code. I imagine IQANdesign's format must be different, but it may be possible to transform a state diagram into Copilot with very little work so that they could benefit from the verification aspect without compromising their usability needs.
I am considering using Copilot for my next project to interpret user-customizable control-flow models. However, my focus has been on the lower levels so far.
That's great! Let me know how it goes.
I've just looked back over your FSM API proposal and your post made a lot more sense to me this time. I can't think of anything else it could need.
Does it handle nesting? Clock delays? Preemptive interruption?
I don't know. We haven't done anything specially to handle these case, and I haven't tried it. What would examples of those look like specifically for the case of FSMs?
Is it an RTOS? 🦋
RTOS is not one of the OSs we currently support.
The code we produce is hard realtime, but we don't normally test it on an RTOS.
That being said, there's been prior work on running Copilot-generated code in an RTOS. We are asked about this frequently, so I'd be opening to revisiting this. Licensing can be tricky (VxWorks is expensive), but now we even have Ubuntu RTOS.
On a related note, we've also just started looking into running Copilot in the eBPF (in kernel space).
If this is a use case that would be useful for you, we could have a chat to better understand what would need to be done to support RTOS.
I really appreciate your reply. I think my client has a large amount of trust in big companies (with a lot of users) to be supported long term. Visual representations are more familiar to them, so perceive them as safer.
I imagine IQANdesign's format must be different, but it may be possible to transform a state diagram into Copilot with very little work
This was the idea. Since IQANdesign can export projects to a txt file, I was able to write some rules for automatic testing. Copilot was on the radar, which is how this issue originated.
we don't normally test it on an RTOS.
I mean you could write an RTOS in Copilot; each task is a FSM nested inside a main event-loop FSM. I've been using embassy, an RTOS that uses Rust's async/await to construct this pattern. I only wanted to mention it as a "free idea".
I expect to be using Copilot on Linux next (eBPF support would be great). I'll let you know how it goes.
I really appreciate your reply. I think my client has a large amount of trust in big companies (with a lot of users) to be supported long term.
I understand.
If this comes up in the future, you can tell them that Copilot has been around since 2010, and we have several projects that use Copilot, so we have no reason to believe that the project will stop any time soon.
This was the idea. Since IQANdesign can export projects to a txt file, I was able to write some rules for automatic testing.
If you have any code that can convert from that format to Copilot (even if WIP/incomplete), it'd be amazing if you could free it. That way, maybe others can use it.
But 100% understandable if that's not an option.
I mean you could write an RTOS in Copilot; each task is a FSM nested inside a main event-loop FSM.
Oh. I hadn't thought about looking at these systems that way. I'll take a look.
I expect to be using Copilot on Linux next (eBPF support would be great). I'll let you know how it goes.
Sounds good.
Whatever comes out of our eBPF work will hopefully also be made public.
Even though this was not used for this project, I think it would still be useful to add this functionality to copilot-libraries. The need has come up in the past in work with LaRC.
Tagging @fdedden and @RyanGlScott for opinions. Also see the implementation above; there may be a better API we want to consider.
I'm not sure if I have a strong opinion about which of the APIs proposed above is best, since I've never tried to use this code in practice. I imagine each encoding would have various strengths and weaknesses, so having some user experience to draw on would be helpful to determine which one is the nicest to use in practice.
I do wonder if we can generalize the code above to work over more types than just Word8. I could foresee it being annoying having to manually convert between, say, 0<->"door closed" and 1<->"door open" (or something like this), but it's hard to say for sure without trying it.
@RyanGlScott This is partly due to our limited ability to support more types (#58 comes to mind).
That being said, if the type is an enum or there is an obvious conversion to numbers, we could definitely re-write it to support anything that can be represented numerically.
@liamdiprose I've been experimenting with converting different formats to these state machines. I have a very crude version of Graphviz -> Copilot, and a while back I implemented support for converting SysML diagrams to stream-based programs.
If you were to use something like this, what would be your tool of choice to describe your diagrams in?
I personally love mermaid/graphviz, so I find your recent progress exiting.
If you were to use something like this, what would be your tool of choice to describe your diagrams in?
I would describe my diagrams as RDF in a graph database, with the understanding that I would have to transform the representation into something standard.
I understand Mermaid, but I was attracted to Copilot because of Haskell and it's rigid type system; the language feels like solid ground to me. So I think I prefer to transform directly to Copilot. If you have a mermaid-like eDSL, that would be great.
Activity
ivanperez-keera commentedon May 11, 2023
Yes. We have done it before. Can you describe your use case more?
liamdiprose commentedon May 11, 2023
Thank you for your reply. For an example, consider an air-lock on a spacecraft, two doors and an intermediate chamber. How does Copilot remember if the chamber is pressurizing or depressurizing?
You could have the trigger functions modify a
stateglobal variable. I was wondering if there was a better approach, say with Temporal Logic?Edit: the use case is a charging protocol on an electric vehicle (i.e. voltage instead of pressure).
ivanperez-keera commentedon Aug 10, 2023
I was hoping to have more time to clean this and improve it, but you've been patiently waiting for over 2 months now, so I'd rather keep things moving than stall this forever. Perfect is the enemy of good!
You can write state machines manually as follows. Let's imagine that you have an incoming stream of inputs with possible values 1, 2 and 3 ONLY:
The values in the list are just for testing purposes.
You can implement the following state machine:
graph TD; 1-->|2|2; 2-->|2|3; 3-->|2|3; 3-->|1|4; 4-->|3|4;With the code:
More generally, here are three possible ways of implementing state machines, depending on whether you consider the existence of a state denoting an error or not, and whether you want all inputs to produce a transition or not.
{-# LANGUAGE DataKinds #-} import Copilot.Language hiding (max, min) import Language.Copilot hiding (max, min) import Prelude hiding ( not, until, (&&), (++), (/=), (==), (||), mod, (>), max, min) -- Initial state, final state, states and transitions, wrong state indicator type StateMachine = ( Word8, Word8, [Word8], [(Word8, Word8, Word8)], Word8 ) stateMachine :: StateMachine -> Stream Word8 -> Stream Word8 stateMachine (initialState, finalState, inputs, transitions, badState) inputSignal = state where state = [initialState] ++ ifThenElses inputs finalState transitions badState inputSignal ifThenElses :: [Word8] -> Word8 -> [(Word8, Word8, Word8)] -> Word8 -> Stream Word8 -> Stream Word8 ifThenElses inputs finalState [] badState inputSignal = ifThenElse (state == constant finalState && noneOf inputSignal inputs) (constant finalState) (constant badState) ifThenElses inputs finalState ((s1,i,s2):ss) badState inputSignal = ifThenElse (state == constant s1 && inputSignal == constant i) (constant s2) (ifThenElses inputs finalState ss badState inputSignal) -- Initial state, final state, transitions type StateMachineG = ( Word8, Word8, [(Word8, Stream Bool, Word8)] ) stateMachineG :: StateMachineG -> Stream Word8 stateMachineG (initialState, finalState, transitions) = state where state = [initialState] ++ ifThenElses finalState transitions ifThenElses :: Word8 -> [(Word8, Stream Bool, Word8)] -> Stream Word8 ifThenElses finalState [] = constant finalState ifThenElses finalState ((s1,i,s2):ss) = ifThenElse (state == constant s1 && i) (constant s2) (ifThenElses finalState ss) -- Initial state, final state, no transition signal, transitions, bad state type StateMachineGF = ( Word8, Word8, Stream Bool, [(Word8, Stream Bool, Word8)], Word8) stateMachineGF :: StateMachineGF -> Stream Word8 stateMachineGF (initialState, finalState, noInputData, transitions, badState) = state where state = [initialState] ++ ifThenElses transitions ifThenElses :: [(Word8, Stream Bool, Word8)] -> Stream Word8 ifThenElses [] = ifThenElse (state == constant finalState && noInputData) (constant finalState) (constant badState) ifThenElses ((s1,i,s2):ss) = ifThenElse (state == constant s1 && i) (constant s2) (ifThenElses ss) noneOf :: Stream Word8 -> [Word8] -> Stream Bool noneOf input [] = true noneOf input (x:xs) = input /= constant x && noneOf input xsYou can use them as follows:
A good outcome of this discussion would be to extend
copilot-librariesto support state machines.ivanperez-keera commentedon Aug 10, 2023
Before immediately including this, perhaps it would pay off to 1) pick a representation that allows us to analyze the state machine first and ensure it's defined correctly, and 2) pick a Copilot implementation that generates more optimal code.
EDIT: By representation, I mean a datatype.
liamdiprose commentedon Aug 14, 2023
I was very glad to see your reply. Thank you very much for these examples, they're gold to someone just starting out with haskell.
In my use case, it turns out the FSM is managed by another controller and we just need to track its state and do stuff when some transitions occur. So the Copilot code turned out to be very simple; mostly
externs and boolean operations.Are there any downsides to tracking the state within Copilot, as opposed to updating a byte in the trigger functions? What if we want to resume the FSM from flash memory? Is the
step()function normally stateless? My guess at the upside is the FSM operation can be proven easier?ivanperez-keera commentedon Aug 15, 2023
Great!
What do you mean by "Updating a byte in the trigger function"?
This presents an interesting use case that, to the best of my knowledge, has never been studied within Copilot. My first thought is that it may be possible by enclosing any stateful streams in an
ifThenElseas follows:The initial example I wrote could be extended with a reset or re-read from memory setting as follows:
The idea being that, when you want to resume from Flash memory, you just need to set the saved state in a global
saved_state, setresettotrue, and then callstep().In general, you cannot assume that successive calls to
step()are stateless. Each call advances streams one step, and they can refer to past values, so they can be stateful. This is a property of all stream-based or reactive languages (e.g., FRP).You'd have a guarantee that the code generated is hard realtime.
You might also be able to prove certain properties of your FSM if you write it in Copilot, by leveraging the facilities of
copilot-theorem, but I haven't done it. I'd be interested to see which properties you might want to prove.You could of course define FSMs in Haskell using an existing library or custom representation, prove whatever you want statically, and then synthesize a Copilot FSM.
If you are operating in a safety-critical environment, then I'd suggest going down the route of trying to prove your FSM correct.
liamdiprose commentedon Aug 23, 2023
Thank you for your answers. Understanding Copilot as a FRP is really cool and it makes a lot more sense for implementing FSMs than what I led myself to believe. I'm looking forward to using and further understanding these FSM APIs you've shared here.
This question might on a bit of a tangent: is it possible/advisable to map
Stream Word8to Haskell's data types? (e.g. encode a state withIdleinstead of1)?ivanperez-keera commentedon Sep 25, 2023
We've historically used integers and constants instead of enums. You can already use them to some extent, so long as you reduce the final result to word/ints using
fromEnumandtoEnum.I suspect extending Copilot to support any Enums would be simple; you'd mainly need to know what underlying type can be used to represent the enum based on its size. I'd have to look into it in more detail. Related to #36, #58.
Otherwise, how is the FSM work going?
ivanperez-keera commentedon Oct 29, 2023
Circling back. Any updates, @liamdiprose ?
liamdiprose commentedon Oct 30, 2023
Hey @ivanperez-keera,
It pains me to say this, but I haven't made any progress because the client has settled with IQANdesign for now. I haven't been able to convince them of the importance of verified, portable code.
I am considering using Copilot for my next project to interpret user-customizable control-flow models. However, my focus has been on the lower levels so far.
I've just looked back over your FSM API proposal and your post made a lot more sense to me this time. I can't think of anything else it could need. Does it handle nesting? Clock delays? Preemptive interruption? Is it an RTOS? 🦋
ivanperez-keera commentedon Oct 30, 2023
That's absolutely ok. On the one hand, it may just be a better fit for their use case, and that's understandable. On the other, knowing more about this could help us improve in the future.
Has the reasoning behind this been one of user experience? Documentation? Anything else?
For what is worth, I've worked on automatically transforming SysML diagrams to Haskell code. I imagine IQANdesign's format must be different, but it may be possible to transform a state diagram into Copilot with very little work so that they could benefit from the verification aspect without compromising their usability needs.
That's great! Let me know how it goes.
I don't know. We haven't done anything specially to handle these case, and I haven't tried it. What would examples of those look like specifically for the case of FSMs?
RTOS is not one of the OSs we currently support.
The code we produce is hard realtime, but we don't normally test it on an RTOS.
That being said, there's been prior work on running Copilot-generated code in an RTOS. We are asked about this frequently, so I'd be opening to revisiting this. Licensing can be tricky (VxWorks is expensive), but now we even have Ubuntu RTOS.
On a related note, we've also just started looking into running Copilot in the eBPF (in kernel space).
If this is a use case that would be useful for you, we could have a chat to better understand what would need to be done to support RTOS.
liamdiprose commentedon Oct 30, 2023
I really appreciate your reply. I think my client has a large amount of trust in big companies (with a lot of users) to be supported long term. Visual representations are more familiar to them, so perceive them as safer.
This was the idea. Since IQANdesign can export projects to a txt file, I was able to write some rules for automatic testing. Copilot was on the radar, which is how this issue originated.
I mean you could write an RTOS in Copilot; each task is a FSM nested inside a main event-loop FSM. I've been using embassy, an RTOS that uses Rust's async/await to construct this pattern. I only wanted to mention it as a "free idea".
I expect to be using Copilot on Linux next (eBPF support would be great). I'll let you know how it goes.
ivanperez-keera commentedon Oct 30, 2023
I understand.
If this comes up in the future, you can tell them that Copilot has been around since 2010, and we have several projects that use Copilot, so we have no reason to believe that the project will stop any time soon.
If you have any code that can convert from that format to Copilot (even if WIP/incomplete), it'd be amazing if you could free it. That way, maybe others can use it.
But 100% understandable if that's not an option.
Oh. I hadn't thought about looking at these systems that way. I'll take a look.
Sounds good.
Whatever comes out of our eBPF work will hopefully also be made public.
ivanperez-keera commentedon Oct 30, 2023
Even though this was not used for this project, I think it would still be useful to add this functionality to
copilot-libraries. The need has come up in the past in work with LaRC.Tagging @fdedden and @RyanGlScott for opinions. Also see the implementation above; there may be a better API we want to consider.
RyanGlScott commentedon Oct 31, 2023
I'm not sure if I have a strong opinion about which of the APIs proposed above is best, since I've never tried to use this code in practice. I imagine each encoding would have various strengths and weaknesses, so having some user experience to draw on would be helpful to determine which one is the nicest to use in practice.
I do wonder if we can generalize the code above to work over more types than just
Word8. I could foresee it being annoying having to manually convert between, say,0<->"door closed" and1<->"door open" (or something like this), but it's hard to say for sure without trying it.ivanperez-keera commentedon Jan 3, 2024
@RyanGlScott This is partly due to our limited ability to support more types (#58 comes to mind).
That being said, if the type is an enum or there is an obvious conversion to numbers, we could definitely re-write it to support anything that can be represented numerically.
@liamdiprose I've been experimenting with converting different formats to these state machines. I have a very crude version of Graphviz -> Copilot, and a while back I implemented support for converting SysML diagrams to stream-based programs.
If you were to use something like this, what would be your tool of choice to describe your diagrams in?
ivanperez-keera commentedon Jan 3, 2024
I also have a quick Haskell script to go from Mermaid to Copilot. From the following Mermaid diagram (copy of the one above):
graph TD; 1-->|2|2; 2-->|2|3; 3-->|2|3; 3-->|1|4; 4-->|3|4;the script produces:
liamdiprose commentedon Jan 3, 2024
Hey @ivanperez-keera,
I personally love mermaid/graphviz, so I find your recent progress exiting.
I would describe my diagrams as RDF in a graph database, with the understanding that I would have to transform the representation into something standard.
I understand Mermaid, but I was attracted to Copilot because of Haskell and it's rigid type system; the language feels like solid ground to me. So I think I prefer to transform directly to Copilot. If you have a mermaid-like eDSL, that would be great.