F´（F Prime）FPP 内部状态机 choice 选择点转出转移：语法、语义与单元测试验证

F´F PrimeFPP 内部状态机 choice 选择点转出转移语法、语义与单元测试验证【免费下载链接】fprimeF´ - A flight software and embedded systems framework项目地址: https://gitcode.com/GitHub_Trending/fpr/fprimeFPPF Prime Primitives是 F´ 飞行软件框架的建模语言其中state machine状态机为组件内部逻辑提供了声明式建模能力而choice选择点则负责在信号触发转移时根据守卫条件动态决定目标状态。本文以 FppTestProject/FppTest/state_machine/internal/choice 下的测试套件为切入点系统讲解 FPP 内部状态机中 choice 转出转移的完整语法、执行语义、层次嵌套与级联用法并结合单元测试源码说明这些语义是如何被验证的。读完本文你将能够读懂并编写包含 choice 的 FPP 状态机模型并掌握对应的 GTest 单元测试组织方式。一、背景FPP 内部状态机与 choice 选择点F´ 的状态机支持通过.fpp/.fppi文件声明并由自动代码生成器转换为 C 实现组件实现类通过继承自动生成的*StateMachineBase基类接入。在状态机建模中choice是一种特殊节点它本身不是可停留的状态而是转移途中的决策点——当状态因信号触发转移进入 choice 时状态机会求值一个或多个guard守卫根据守卫的真假选择不同的action序列与目标状态。internal/choice目录的 README 将这一主题概括为Tests for transitions out of choices in FPP internal state machines.针对 FPP 内部状态机中从选择点转出转移的测试整个目录围绕从 choice 转出这一核心语义设计了七组状态机模型与对应的 GTest 单元测试覆盖了最简选择、类型化选择、多信号输入、选择点级联、层次嵌套等场景是研究 choice 语义最直接的源码级教材。二、测试套件全景七个场景的目录组织该目录下每个场景都遵循FPP 模型 自动生成绑定 手写测试实现的标准结构场景.fpp / include/*.fppi测试实现.cpp验证的主题BasicBasic.cpp最基本的 choice单守卫、双分支、action 目标状态BasicU32BasicU32.cpp携带U32数据的 signal/guard/action 的 choiceInputPairU16U32InputPairU32.cpp源码见InputPairU16U32.cpp两个不同类型信号U16、U32进入同一 choiceSequenceSequence.cppchoice 到 choice 的级联守卫链式决策SequenceU32SequenceU32.cpp类型化版本的 choice 级联ChoiceToStateChoiceToState.cpp层次状态机中 choice 转入嵌套状态如S2.S3ChoiceToChoiceChoiceToChoice.cpp层次状态机中 choice 转入嵌套 choice如S2.C2每个场景由一个X.fpp顶层文件通过include include/X.fppi引入模型定义例如 Basic.fpp 内容为module FppTest { module SmChoice { include include/Basic.fppi } }module FppTest与module SmChoice两层层级命名空间保证了生成的 C 类型如FppTest::SmChoice::Basic在大型测试工程中不冲突。三、choice 基本语法与执行语义Basicinclude/Basic.fppi 给出了一个最小的、带 choice 的状态机完整定义如下 A basic state machine with a choice state machine Basic { Action a action a Action b action b Signal s signal s Guard g guard g Initial transition initial enter S1 State S1 state S1 { State transition on s enter C } Choice C choice C { if g do { a } enter S2 else do { b } enter S3 } State S2 state S2 State S3 state S3 }这段模型展示了 FPP choice 的全部基础要素signal s外部可注入的输入信号是触发转移的事件。action a/action b转移过程中执行的副作用动作在 C 侧以虚函数形式由使用者实现见下文Basic::action_a。guard g返回布尔值的守卫函数用于在 choice 处做分支决策。initial enter S1状态机启动时进入初始状态S1。state S1 { on s enter C }状态S1声明信号转移——收到s时离开S1进入选择点Cchoice 用enter进入与其他节点一致。choice C { if g do { a } enter S2 else do { b } enter S3 }选择点C的核心语义是求值守卫后转出——守卫g为真时执行动作a并进入S2为假时执行动作b并进入S3。由此可以归纳 choice 的完整执行序列状态机位于S1收到信号s触发on s enter C状态机离开S1若声明了exit动作则先执行退出动作进入选择点C不驻留立即求值守卫g根据g的取值走对应分支执行do { ... }中列出的动作随后通过enter进入目标状态到达目标状态时执行其entry动作如有转移完成。这一守卫即分支的语义使得 choice 等价于状态机内部的动态路由最终目标状态不在模型编译期确定而是在运行期由守卫返回值决定。四、携带数据类型的选择点BasicU32 与 InputPairU16U32真实嵌入式场景中信号与守卫通常需要携带数据。BasicU32与InputPairU16U32两个模型专门测试了类型化输入下 choice 的转出行为。include/BasicU32.fppi 中信号、守卫与动作都携带U32数据action a: U32 signal s: U32 guard g: U32 state S1 { on s enter C } choice C { if g do { a } enter S2 else do { b } enter S3 }这里guard g: U32表示守卫的形参类型为U32即信号s携带的数据会被传递给守卫求值action a: U32表示动作接收U32数据signal s: U32表示注入信号时需附带一个U32值。测试实现中BasicU32::sendSignal_s(value)即以此值触发转移。include/InputPairU16U32.fppi 则进一步测试多个不同类型信号复用到同一个 choiceaction a: U32 signal s1: U16 signal s2: U32 guard g: U32 state S1 { on s1 enter C on s2 enter C } choice C { if g do { a } enter S2 else do { a } enter S3 }该模型中有两个信号s1: U16与s2: U32它们各自声明了指向同一选择点C的转移而 choice 的守卫g与动作a都按U32声明。也就是说无论从哪个信号触发进入C其携带的数据都会被转换为守卫/动作期望的类型后参与决策与动作执行U16数据在传递过程中升级为U32。这一设计验证了 FPP 状态机在类型化输入下的兼容与转换能力为组件内部使用不同位宽测量值、计数器等信号做统一决策提供了依据。五、选择点级联choice 序列Sequence / SequenceU32当单个守卫不足以表达多级分支决策时FPP 允许一个 choice 的分支目标直接是另一个 choice形成级联路由。include/Sequence.fppi 完整展示了这一模式state S1 { on s enter C1 } choice C1 { if g1 enter S2 else enter C2 } choice C2 { if g2 do { a } enter S3 else do { b } enter S4 }执行语义与直觉一致收到s后先进入C1若守卫g1为真直接进入S2不再经过C2若g1为假转入C2随后求值g2为真则执行a进入S3为假则执行b进入S4。这种守卫链的写法把多条件组合决策拆解为顺序判断比在单一 choice 中堆叠复杂布尔表达式更易读、易测。SequenceU32见 include/SequenceU32.fppi是该模式的类型化版本signal s: U32、action a: U32、guard g2: U32而guard g1仍为无参布尔守卫——可见级联中每个守卫可以独立决定是否需要数据混用无参守卫与带参守卫完全合法。六、层次状态机中的选择点ChoiceToState / ChoiceToChoiceFPP 状态机支持状态嵌套层次化choice 的转出目标因此也可以指向嵌套状态甚至嵌套 choice。这两个模型专门验证带层次的 choice 转出。choice 转入嵌套状态ChoiceToStateinclude/ChoiceToState.fppi 中选择点C的一个分支目标是嵌套状态S2.S3state S1 { exit do { exitS1 } choice C { if g do { a } enter S2 else do { a } enter S2.S3 } on s enter C } state S2 { entry do { enterS2 } initial do { a } enter S3 state S3 { entry do { enterS3 } } }该模型验证了两个要点choice 分支可直达任意深度的嵌套状态enter S2.S3会依次进入父状态S2与子状态S3并触发各自的entry动作enterS2、enterS3以从外向里的顺序执行退出动作与入口动作的配合S1声明了exit do { exitS1 }因此无论走哪个分支从S1转出时都会先执行exitS1S2还带有自己的initial转移initial do { a } enter S3用于无外部输入时确定嵌套初始状态。choice 转入嵌套 choiceChoiceToChoiceinclude/ChoiceToChoice.fppi 更进一步把层级与级联合并——外层的 choice 分支目标是内层的 choicestate S1 { exit do { exitS1 } choice C1 { if g1 do { a } enter S2 else do { a } enter S2.C2 } on s enter C1 } state S2 { entry do { enterS2 } initial enter S3 choice C2 { if g2 enter S3 else enter S4 } state S3 state S4 }对应运行路径为g1为真执行a后进入父状态S2随后由S2的initial转移进入S3g1为假执行a后进入S2.C2即S2内部的嵌套选择点此时不触发S2的initial转移而是立即求值g2为真进入S3为假进入S4。由此可见 FPP 的完整路由规则进入嵌套 choice 会跳过父状态的 initial 转移直接把决策权交给内层 choice只有直接进入父状态本身时父状态的initial才生效。这一细节对设计层次状态机至关重要正是ChoiceToChoice三个测试用例G1True、G1FalseG2True、G1FalseG2False逐一验证的分支组合。七、单元测试如何验证 choice 语义测试实现动作记录与守卫桩每个场景的.cpp都通过记录调用历史 可编程守卫返回值的方式断言 choice 行为。以 Basic.cpp 为例void Basic::action_a(Signal signal) { this-m_action_a_history.push(signal); } void Basic::action_b(Signal signal) { this-m_action_b_history.push(signal); } bool Basic::guard_g(Signal signal) const { return this-m_guard_g.call(signal); }实现类重写自动生成基类BasicStateMachineBase的action_a、action_b、guard_g虚接口把动作调用压入历史栈把守卫调用转发给可编程桩m_guard_g可预设返回值并记录调用历史。testTrue守卫恒真路径的断言序列完整复现了 choice 语义this-m_guard_g.setReturnValue(true); const FwEnumStoreType id SmHarness::Pick::stateMachineId(); this-initBase(id); ASSERT_EQ(this-getState(), State::S1); this-sendSignal_s(); this-sendSignal_s(); ASSERT_EQ(this-m_guard_g.getCallHistory().getSize(), 1); ASSERT_EQ(this-m_guard_g.getCallHistory().getItemAt(0), Signal::s); ASSERT_EQ(this-m_action_a_history.getSize(), 1); ASSERT_EQ(this-m_action_a_history.getItemAt(0), Signal::s); ASSERT_EQ(this-m_action_b_history.getSize(), 0); ASSERT_EQ(this-getState(), State::S2);几点值得注意的验证手法状态断言initBase后断言位于S1sendSignal_s()两次后断言位于S2守卫为真分支守卫调用次数两次sendSignal_s只触发一次守卫求值——因为状态机首次收到s后已从S1转移到S2S2未声明on s转移故第二次信号不再触发 choice动作历史断言action_a恰好被调用一次、action_b从未被调用并核对传入的信号值守卫桩调用历史断言守卫收到的正是信号s验证了信号到守卫的参数传递。对称的testFalsesetReturnValue(false)断言action_b被调用一次、action_a未被调用最终状态为S3。测试用例清单与随机化main.cpp 把七个场景的所有分支路径组织为 16 个 GTest 用例场景用例BasicTrue、FalseBasicU32True、FalseInputPairU16U32S1True、S1False、S2True、S2FalseChoiceToChoiceG1True、G1FalseG2True、G1FalseG2FalseChoiceToStateTrue、FalseSequenceG1True、G1FalseG2True、G1FalseG2FalseSequenceU32G1True、G1FalseG2True、G1FalseG2False用例命名直接映射分支路径如G1FalseG2True表示守卫 1 为假、守卫 2 为真的组合。main函数在运行全部测试前调用STest::Random::seed()见 STest/STest/Random用随机种子初始化状态机 ID 等 harness 参数兼顾确定性与覆盖度。八、构建与运行该目录的 CMakeLists.txt 展示了 F´ 状态机测试模块的标准组织方式set(SOURCE_FILES ${CMAKE_CURRENT_LIST_DIR}/Basic.fpp ${CMAKE_CURRENT_LIST_DIR}/BasicU32.fpp ... ) set(MOD_DEPS FppTest/state_machine/internal/harness) register_fprime_module() set(UT_SOURCE_FILES ${CMAKE_CURRENT_LIST_DIR}/Basic.cpp ... ${CMAKE_CURRENT_LIST_DIR}/main.cpp ) set(UT_MOD_DEPS STest) register_fprime_ut()要点register_fprime_module()把 7 个.fpp模型注册为库模块由 FPP 自动代码生成器产出状态机基类MOD_DEPS FppTest/state_machine/internal/harness依赖同一状态机测试体系下的 harness 模块提供SmHarness::Pick::stateMachineId()等随机选择工具register_fprime_ut()注册 GTest 单元测试目标UT_MOD_DEPS STest引入 STest 测试基础设施随机、Pick、场景等工具见 STest/STest。在 F´ 工程中可通过fprime-util build --ut构建单元测试、fprime-util check运行包含该套件在内的全部测试F´ 的标准构建/测试工具链用法参见 docs/user-manual 与 cmake 下的fprime-util.cmake。运行后 16 个用例会以 GTest 标准输出逐个报告任何守卫分支或动作序列不符合预期都会导致对应断言失败。九、总结通过internal/choice这一测试套件可以完整掌握 FPP 内部状态机中 choice 转出转移的建模与验证方法语法choice C { if g do { a } enter S2 else do { b } enter S3 }分支可带动作序列目标可为状态或嵌套状态语义choice 不驻留进入后立即求值守卫并转出运行期决定目标状态类型化signal/guard/action 均可携带U32等数据类型多个不同类型信号可复用同一 choice级联choice 分支可指向另一 choice形成守卫链式决策Sequence、SequenceU32层次enter S2.S3直达嵌套状态enter S2.C2直达嵌套 choice 并跳过父状态 initialChoiceToState、ChoiceToChoice验证通过动作历史、守卫桩与状态断言把每条分支路径固化为独立 GTest 用例。这些模型与测试既是 FPP 状态机语言能力的实证也是开发者编写自定义状态机组件时的可靠参照。【免费下载链接】fprimeF´ - A flight software and embedded systems framework项目地址: https://gitcode.com/GitHub_Trending/fpr/fprime创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考