• luafaudes
• Introduction  
• Lua-Console  
• Lua-Extensions  
• Technical Detail  
•  
• Tutorials
• 1_containers.lua  
• 2_generators.lua  
• 3_regular.lua  
• 4_composition.lua  
• 5_faulttolerant.lua  
• 6_algorithm.lua  
• decdemo_verify.lua  
• diag_1_event.lua  
• diag_2_language.lua  
• diag_3_modular.lua  
• elevator_synthesis.lua  
• ftc_tutorial_models.lua  
• ftc_tutorial_reconf.lua  
• hio_1_introduction.lua  
• hio_2_hiogenerators.lua  
• hio_3_hiofunctions.lua  
• hio_4_transport_unit.lua  
• ios_1_system.lua  
• mtc_1_generators.lua  
• mtc_2_functions.lua  
• mtc_3_observer.lua  
• op_fsmsynth_ds.lua  
• op_fsmsynth_exit1.lua  
• op_fsmsynth_exit2.lua  
• op_fsmsynth_ics.lua  
• op_fsmsynth_ms.lua  
• op_fsmsynth_pc1.lua  
• op_fsmsynth_pc1_exit1_ics.lua  
• op_fsmsynth_pc2.lua  
• pev_2_verify.lua  
• pev_cbs_setup.lua  
• syn_1_simple.lua  
• syn_3_reduction.lua  
• syn_4_validate.lua  
• syn_5_stdcons.lua  

luafaudes Tutorial: pev_2_verify.lua

To run the below Lua script, cd to the tutorial section of the respective plug-in and enter luafaudes pev_2_verify.lua at the command prompt. The script will read input data from ./tutorial/data/.

-- Conveyor Belts Demo for Compositional Verification
--
-- Uses "pev_cbs_setup.lua" to generate the models


-- configure number of conveyor belts via command line, default to 5
N=arg[1]
if N == nil then N=5 end  
print(string.format('pev_2_verify.lua: number of conveyor belts N=%d',N))

-- generate models
dofile("pev_cbs_setup.lua")

-- read models
print('pev_2_verify.lua: reading models')
gvec=faudes.GeneratorVector()
gvec:Append('tmp_pev_cbs_src.gen')
for i=1,N do
  gvec:Append(string.format('tmp_pev_cbs_%d_cl.gen',i))
end
gvec:Append("tmp_pev_cbs_snk.gen")

-- read priorities
prios = faudes.EventPriorities("tmp_pev_cbs_prios.alph");

-- do verify (compositional)
print('pev_2_verify.lua: compositional verification')
isnc = faudes.IsPNonblocking(gvec,prios)
if isnc then
  print('pev_2_verify: nonconflictingness confirmed (PASS)')
else
  print('pev_2_verify: nonconflictingness failed (FAIL)')
end
FAUDES_TEST_DUMP("prio comp ver",isnc)

-- do verify (monolitic, for limited number of conveyor belts)
if tonumber(N) <6 then
  print('pev_2_verify.lua: monolitic verification')
  gall=faudes.Generator()
  faudes.ParallelNB(gvec,gall)
  print('pev_2_verify: overall statecount:',gall:Size())
  faudes.ShapePriorities(gall,prios)
  isnc = faudes.IsNonblocking(gall)
  if isnc then
    print('pev_2_verify: nonconflictingness confirmed (PASS)')
  else
    print('pev_2_verify: nonconflictingness failed (FAIL)')
  end
end

libFAUDES 2.33c --- 2025.05.15 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-priorities-luabindings-hybrid-example-pybindings"